Let X and Tx be given.
Assume HTxeq: Tx = discrete_topology X.
Assume HTx: topology_on X Tx.
We will prove covering_dimension X Tx Empty.
Set B to be the term singleton_basis X.
We will prove (topology_on X Tx ∧ Empty ∈ ω) ∧ ∀A : set, open_cover_of X Tx A → ∃B0 : set, open_cover_of X Tx B0 ∧ refines_cover B0 A ∧ collection_has_order_at_most_m_plus_one X B0 Empty.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Let A be given.
Assume HA: open_cover_of X Tx A.
We use B to witness the existential quantifier.
We will prove open_cover_of X Tx B ∧ refines_cover B A ∧ collection_has_order_at_most_m_plus_one X B Empty.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove open_cover_of X Tx B.
We will prove ((topology_on X Tx ∧ B ⊆ 𝒫 X) ∧ X ⊆ ⋃ B) ∧ (∀U : set, U ∈ B → U ∈ Tx).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is (basis_on_sub_Power X B (singleton_basis_is_basis X)).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ B.
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b.
An exact proof term for the current goal is (basis_on_cover X B (singleton_basis_is_basis X) x HxX).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair: b ∈ B ∧ x ∈ b.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b) Hbpair).
An exact proof term for the current goal is (UnionI B x b Hxb HbB).
Let U be given.
Assume HU: U ∈ B.
We will prove U ∈ Tx.
We prove the intermediate claim HU0: U ∈ 𝒫 X.
An exact proof term for the current goal is ((basis_on_sub_Power X B (singleton_basis_is_basis X)) U HU).
rewrite the current goal using HTxeq (from left to right).
An exact proof term for the current goal is HU0.
We will prove refines_cover B A.
Let U be given.
Assume HU: U ∈ B.
Apply (ReplE_impred X (λx0 : set ⇒ {x0}) U HU (∃V : set, V ∈ A ∧ U ⊆ V)) to the current goal.
Let u0 be given.
Assume Hu0X: u0 ∈ X.
Assume HUeq: U = {u0}.
We prove the intermediate claim Hcov: X ⊆ ⋃ A.
An exact proof term for the current goal is (open_cover_of_covers X Tx A HA).
We prove the intermediate claim Hu0Union: u0 ∈ ⋃ A.
An exact proof term for the current goal is (Hcov u0 Hu0X).
Apply (UnionE_impred A u0 Hu0Union (∃V : set, V ∈ A ∧ U ⊆ V)) to the current goal.
Let V be given.
Assume HV: u0 ∈ V.
Assume HVA: V ∈ A.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVA.
Let y be given.
Assume HyU: y ∈ U.
We will prove y ∈ V.
We prove the intermediate claim HyU0: y ∈ {u0}.
We will prove y ∈ {u0}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HyU.
We prove the intermediate claim Hyu0: y = u0.
An exact proof term for the current goal is (SingE u0 y HyU0).
rewrite the current goal using Hyu0 (from left to right).
An exact proof term for the current goal is HV.
We will prove collection_has_order_at_most_m_plus_one X B Empty.
We will prove ordinal Empty ∧ ∀x : set, x ∈ X → cardinality_at_most {U ∈ B|x ∈ U} (ordsucc Empty).
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).
Let x be given.
Assume HxX: x ∈ X.
We will prove cardinality_at_most {U ∈ B|x ∈ U} (ordsucc Empty).
Set Sx to be the term {U ∈ B|x ∈ U}.
We prove the intermediate claim HSx: Sx = {{x}}.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ Sx.
We will prove U ∈ {{x}}.
We prove the intermediate claim HU0: U ∈ B.
An exact proof term for the current goal is (SepE1 B (λU0 : set ⇒ x ∈ U0) U HU).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepE2 B (λU0 : set ⇒ x ∈ U0) U HU).
Apply (ReplE_impred X (λx0 : set ⇒ {x0}) U HU0 (U ∈ {{x}})) to the current goal.
Let u0 be given.
Assume Hu0X: u0 ∈ X.
Assume HUeq: U = {u0}.
We prove the intermediate claim Hxu0: x = u0.
We prove the intermediate claim HxU0: x ∈ {u0}.
We will prove x ∈ {u0}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (SingE u0 x HxU0).
rewrite the current goal using HUeq (from left to right).
rewrite the current goal using Hxu0 (from right to left).
An exact proof term for the current goal is (SingI {x}).
Let U be given.
Assume HU: U ∈ {{x}}.
We will prove U ∈ Sx.
We prove the intermediate claim HUeq: U = {x}.
An exact proof term for the current goal is (SingE {x} U HU).
rewrite the current goal using HUeq (from left to right).
Apply (SepI B (λU0 : set ⇒ x ∈ U0) {x}) to the current goal.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ {x0}) x HxX).
An exact proof term for the current goal is (SingI x).
We will prove cardinality_at_most Sx (ordsucc 0).
We will prove ordinal (ordsucc 0) ∧ ∃k : set, ordinal k ∧ k ⊆ ordsucc 0 ∧ equip Sx k.
Apply andI to the current goal.
An exact proof term for the current goal is (ordinal_ordsucc 0 (nat_p_ordinal 0 nat_0)).
We use (ordsucc 0) to witness the existential quantifier.
We will prove ordinal (ordsucc 0) ∧ (ordsucc 0) ⊆ ordsucc 0 ∧ equip Sx (ordsucc 0).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (ordinal_ordsucc 0 (nat_p_ordinal 0 nat_0)).
An exact proof term for the current goal is (Subq_ref (ordsucc 0)).
rewrite the current goal using HSx (from left to right).
An exact proof term for the current goal is (equip_Sing_1 {x}).
∎