Let X, Tx, Fam and n be given.
Assume HTx: topology_on X Tx.
Assume HnO: n ∈ ω.
Assume Hfin: finite Fam.
Assume Hfam: ∀Y : set, Y ∈ Fam → Y ⊆ X ∧ closed_in X Tx Y ∧ covering_dimension Y (subspace_topology X Tx Y) n.
Set p to be the term λF0 : set ⇒ (∀Y : set, Y ∈ F0 → Y ⊆ X ∧ closed_in X Tx Y ∧ covering_dimension Y (subspace_topology X Tx Y) n) → covering_dimension (⋃ F0) (subspace_topology X Tx (⋃ F0)) n.
We prove the intermediate claim HpEmpty: p Empty.
Assume Hall0: ∀Y : set, Y ∈ Empty → Y ⊆ X ∧ closed_in X Tx Y ∧ covering_dimension Y (subspace_topology X Tx Y) n.
rewrite the current goal using Union_Empty_eq (from left to right).
Set T0 to be the term subspace_topology X Tx Empty.
We prove the intermediate claim HEmptySubX: Empty ⊆ X.
Let x be given.
Assume Hx: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) Hx).
We prove the intermediate claim HT0: topology_on Empty T0.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Empty HTx HEmptySubX).
We will prove covering_dimension Empty T0 n.
Apply (covering_dimensionI Empty T0 n) to the current goal.
An exact proof term for the current goal is HT0.
An exact proof term for the current goal is HnO.
Let A be given.
Assume HA: open_cover_of Empty T0 A.
We use Empty to witness the existential quantifier.
We will prove open_cover_of Empty T0 Empty ∧ refines_cover Empty A ∧ collection_has_order_at_most_m_plus_one Empty Empty n.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (open_cover_ofI Empty T0 Empty) to the current goal.
An exact proof term for the current goal is HT0.
Let U be given.
Assume HU: U ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE U) HU).
rewrite the current goal using Union_Empty_eq (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
Let U be given.
Assume HU: U ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE U) HU).
Let U be given.
Assume HU: U ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE U) HU).
We will prove collection_has_order_at_most_m_plus_one Empty Empty n.
We will prove ordinal n ∧ ∀x : set, x ∈ Empty → cardinality_at_most {U ∈ Empty|x ∈ U} (ordsucc n).
Apply andI to the current goal.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
Let x be given.
Assume Hx: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) Hx).
We prove the intermediate claim HpStep: ∀F0 y : set, finite F0 → y ∉ F0 → p F0 → p (F0 ∪ {y}).
Let F0 and y be given.
Assume HF0fin: finite F0.
Assume HyNot: y ∉ F0.
Assume IH: p F0.
Assume HallU: ∀Y : set, Y ∈ (F0 ∪ {y}) → Y ⊆ X ∧ closed_in X Tx Y ∧ covering_dimension Y (subspace_topology X Tx Y) n.
We prove the intermediate claim HallF0: ∀Y : set, Y ∈ F0 → Y ⊆ X ∧ closed_in X Tx Y ∧ covering_dimension Y (subspace_topology X Tx Y) n.
Let Y be given.
Assume HYF0: Y ∈ F0.
An exact proof term for the current goal is (HallU Y (binunionI1 F0 {y} Y HYF0)).
We prove the intermediate claim HdimF0: covering_dimension (⋃ F0) (subspace_topology X Tx (⋃ F0)) n.
An exact proof term for the current goal is (IH HallF0).
We prove the intermediate claim HUnionF0subX: (⋃ F0) ⊆ X.
Let x be given.
Assume HxUF0: x ∈ ⋃ F0.
Apply (UnionE_impred F0 x HxUF0 (x ∈ X)) to the current goal.
Let Y be given.
Assume HxY: x ∈ Y.
Assume HYF0: Y ∈ F0.
We prove the intermediate claim HYpack: (Y ⊆ X ∧ closed_in X Tx Y) ∧ covering_dimension Y (subspace_topology X Tx Y) n.
An exact proof term for the current goal is (HallF0 Y HYF0).
We prove the intermediate claim HYsubcl: Y ⊆ X ∧ closed_in X Tx Y.
An exact proof term for the current goal is (andEL (Y ⊆ X ∧ closed_in X Tx Y) (covering_dimension Y (subspace_topology X Tx Y) n) HYpack).
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (andEL (Y ⊆ X) (closed_in X Tx Y) HYsubcl).
An exact proof term for the current goal is (HYsub x HxY).
We prove the intermediate claim HallClosedF0: ∀C : set, C ∈ F0 → closed_in X Tx C.
Let C be given.
Assume HCF0: C ∈ F0.
We prove the intermediate claim HCpack: (C ⊆ X ∧ closed_in X Tx C) ∧ covering_dimension C (subspace_topology X Tx C) n.
An exact proof term for the current goal is (HallF0 C HCF0).
We prove the intermediate claim HCsubcl: C ⊆ X ∧ closed_in X Tx C.
An exact proof term for the current goal is (andEL (C ⊆ X ∧ closed_in X Tx C) (covering_dimension C (subspace_topology X Tx C) n) HCpack).
An exact proof term for the current goal is (andER (C ⊆ X) (closed_in X Tx C) HCsubcl).
We prove the intermediate claim HUnionF0closed: closed_in X Tx (⋃ F0).
An exact proof term for the current goal is (finite_union_closed_in X Tx F0 HTx HF0fin HallClosedF0).
We prove the intermediate claim Hypack: (y ⊆ X ∧ closed_in X Tx y) ∧ covering_dimension y (subspace_topology X Tx y) n.
An exact proof term for the current goal is (HallU y (binunionI2 F0 {y} y (SingI y))).
We prove the intermediate claim Hysubcl: y ⊆ X ∧ closed_in X Tx y.
An exact proof term for the current goal is (andEL (y ⊆ X ∧ closed_in X Tx y) (covering_dimension y (subspace_topology X Tx y) n) Hypack).
We prove the intermediate claim Hysub: y ⊆ X.
An exact proof term for the current goal is (andEL (y ⊆ X) (closed_in X Tx y) Hysubcl).
We prove the intermediate claim HyClosed: closed_in X Tx y.
An exact proof term for the current goal is (andER (y ⊆ X) (closed_in X Tx y) Hysubcl).
We prove the intermediate claim Hdimy: covering_dimension y (subspace_topology X Tx y) n.
An exact proof term for the current goal is (andER (y ⊆ X ∧ closed_in X Tx y) (covering_dimension y (subspace_topology X Tx y) n) Hypack).
rewrite the current goal using (Union_binunion_singleton_eq F0 y) (from left to right).
An exact proof term for the current goal is (dimension_union_closed_max X Tx (⋃ F0) y n HTx HUnionF0subX Hysub HUnionF0closed HyClosed HdimF0 Hdimy).
We prove the intermediate claim HpFam: p Fam.
An exact proof term for the current goal is (finite_ind p HpEmpty HpStep Fam Hfin).
An exact proof term for the current goal is (HpFam Hfam).
∎