Let X, Tx, Y, Z and n be given.
Assume HTx: topology_on X Tx.
Assume HYsub: Y ⊆ X.
Assume HZsub: Z ⊆ X.
Assume HYcl: closed_in X Tx Y.
Assume HZcl: closed_in X Tx Z.
Assume HdimY: covering_dimension Y (subspace_topology X Tx Y) n.
Assume HdimZ: covering_dimension Z (subspace_topology X Tx Z) n.
Set W to be the term Y ∪ Z.
We prove the intermediate claim HWsubX: W ⊆ X.
Let x be given.
Assume HxW: x ∈ W.
Apply (binunionE Y Z x HxW (x ∈ X)) to the current goal.
Assume HxY: x ∈ Y.
An exact proof term for the current goal is (HYsub x HxY).
Assume HxZ: x ∈ Z.
An exact proof term for the current goal is (HZsub x HxZ).
We prove the intermediate claim HTw: topology_on W (subspace_topology X Tx W).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx W HTx HWsubX).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (covering_dimension_n_in_omega Y (subspace_topology X Tx Y) n HdimY).
We will prove covering_dimension W (subspace_topology X Tx W) n.
Apply (covering_dimensionI W (subspace_topology X Tx W) n) to the current goal.
An exact proof term for the current goal is HTw.
An exact proof term for the current goal is HnO.
Let A be given.
Assume HA: open_cover_of W (subspace_topology X Tx W) A.
Set Tw0 to be the term subspace_topology X Tx W.
We prove the intermediate claim HYsubW: Y ⊆ W.
Let y be given.
Assume HyY: y ∈ Y.
An exact proof term for the current goal is (binunionI1 Y Z y HyY).
We prove the intermediate claim HZsubW: Z ⊆ W.
Let z be given.
Assume HzZ: z ∈ Z.
An exact proof term for the current goal is (binunionI2 Y Z z HzZ).
Set Ty to be the term subspace_topology X Tx Y.
Set Tz to be the term subspace_topology X Tx Z.
We prove the intermediate claim HTwyEq: subspace_topology W Tw0 Y = Ty.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx W Y HTx HWsubX HYsubW).
We prove the intermediate claim HTwzEq: subspace_topology W Tw0 Z = Tz.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx W Z HTx HWsubX HZsubW).
We prove the intermediate claim HdimYprop: ∀A0 : set, open_cover_of Y Ty A0 → ∃B0 : set, open_cover_of Y Ty B0 ∧ refines_cover B0 A0 ∧ collection_has_order_at_most_m_plus_one Y B0 n.
Apply HdimY to the current goal.
Assume Hcore Hrest.
An exact proof term for the current goal is Hrest.
We prove the intermediate claim HdimZprop: ∀A0 : set, open_cover_of Z Tz A0 → ∃B0 : set, open_cover_of Z Tz B0 ∧ refines_cover B0 A0 ∧ collection_has_order_at_most_m_plus_one Z B0 n.
Apply HdimZ to the current goal.
Assume Hcore Hrest.
An exact proof term for the current goal is Hrest.
Set AY to be the term restrict_family_to_subspace A Y.
We prove the intermediate claim HAYw: open_cover_of Y (subspace_topology W Tw0 Y) AY.
An exact proof term for the current goal is (open_cover_of_restrict_to_subspace W Tw0 A Y HA HYsubW).
We prove the intermediate claim HAY: open_cover_of Y Ty AY.
rewrite the current goal using HTwyEq (from right to left).
An exact proof term for the current goal is HAYw.
We prove the intermediate claim HexBY: ∃BY : set, open_cover_of Y Ty BY ∧ refines_cover BY AY ∧ collection_has_order_at_most_m_plus_one Y BY n.
An exact proof term for the current goal is (HdimYprop AY HAY).
Set AZ to be the term restrict_family_to_subspace A Z.
We prove the intermediate claim HAZw: open_cover_of Z (subspace_topology W Tw0 Z) AZ.
An exact proof term for the current goal is (open_cover_of_restrict_to_subspace W Tw0 A Z HA HZsubW).
We prove the intermediate claim HAZ: open_cover_of Z Tz AZ.
rewrite the current goal using HTwzEq (from right to left).
An exact proof term for the current goal is HAZw.
We prove the intermediate claim HexBZ: ∃BZ : set, open_cover_of Z Tz BZ ∧ refines_cover BZ AZ ∧ collection_has_order_at_most_m_plus_one Z BZ n.
An exact proof term for the current goal is (HdimZprop AZ HAZ).
Apply HexBY to the current goal.
Let BY be given.
Assume HBYpack: open_cover_of Y Ty BY ∧ refines_cover BY AY ∧ collection_has_order_at_most_m_plus_one Y BY n.
Apply HexBZ to the current goal.
Let BZ be given.
Assume HBZpack: open_cover_of Z Tz BZ ∧ refines_cover BZ AZ ∧ collection_has_order_at_most_m_plus_one Z BZ n.
We prove the intermediate claim HBYpair: open_cover_of Y Ty BY ∧ refines_cover BY AY.
An exact proof term for the current goal is (andEL (open_cover_of Y Ty BY ∧ refines_cover BY AY) (collection_has_order_at_most_m_plus_one Y BY n) HBYpack).
We prove the intermediate claim HBZpair: open_cover_of Z Tz BZ ∧ refines_cover BZ AZ.
An exact proof term for the current goal is (andEL (open_cover_of Z Tz BZ ∧ refines_cover BZ AZ) (collection_has_order_at_most_m_plus_one Z BZ n) HBZpack).
We prove the intermediate claim HBYord: collection_has_order_at_most_m_plus_one Y BY n.
An exact proof term for the current goal is (andER (open_cover_of Y Ty BY ∧ refines_cover BY AY) (collection_has_order_at_most_m_plus_one Y BY n) HBYpack).
We prove the intermediate claim HBZord: collection_has_order_at_most_m_plus_one Z BZ n.
An exact proof term for the current goal is (andER (open_cover_of Z Tz BZ ∧ refines_cover BZ AZ) (collection_has_order_at_most_m_plus_one Z BZ n) HBZpack).
We prove the intermediate claim HBYcov: open_cover_of Y Ty BY.
An exact proof term for the current goal is (andEL (open_cover_of Y Ty BY) (refines_cover BY AY) HBYpair).
We prove the intermediate claim HBYref: refines_cover BY AY.
An exact proof term for the current goal is (andER (open_cover_of Y Ty BY) (refines_cover BY AY) HBYpair).
We prove the intermediate claim HBZcov: open_cover_of Z Tz BZ.
An exact proof term for the current goal is (andEL (open_cover_of Z Tz BZ) (refines_cover BZ AZ) HBZpair).
We prove the intermediate claim HBZref: refines_cover BZ AZ.
An exact proof term for the current goal is (andER (open_cover_of Z Tz BZ) (refines_cover BZ AZ) HBZpair).
Set WYc to be the term W ∖ Y.
We prove the intermediate claim HWYopen: WYc ∈ Tw0.
Set V to be the term X ∖ Y.
We prove the intermediate claim HVopenIn: open_in X Tx V.
An exact proof term for the current goal is (open_of_closed_complement X Tx Y HYcl).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx V HVopenIn).
We prove the intermediate claim HVsubW: (V ∩ W) ∈ Tw0.
An exact proof term for the current goal is (subspace_topologyI X Tx W V HVTx).
We prove the intermediate claim HWYeq: WYc = V ∩ W.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ WYc.
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (setminusE1 W Y x Hx).
We prove the intermediate claim HxnotY: x ∉ Y.
An exact proof term for the current goal is (setminusE2 W Y x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HWsubX x HxW).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (setminusI X Y x HxX HxnotY).
An exact proof term for the current goal is (binintersectI V W x HxV HxW).
Let x be given.
Assume Hx: x ∈ V ∩ W.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V W x Hx).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (binintersectE2 V W x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HWsubX x HxW).
We prove the intermediate claim HxnotY: x ∉ Y.
An exact proof term for the current goal is (setminusE2 X Y x HxV).
An exact proof term for the current goal is (setminusI W Y x HxW HxnotY).
An exact proof term for the current goal is (eq_subst_mem WYc (V ∩ W) Tw0 HWYeq HVsubW).
We prove the intermediate claim HAopen: ∀U : set, U ∈ A → U ∈ Tw0.
Let U be given.
Assume HU: U ∈ A.
An exact proof term for the current goal is (open_cover_of_members_open W Tw0 A U HA HU).
We prove the intermediate claim HAsubPow: A ⊆ 𝒫 W.
An exact proof term for the current goal is (open_cover_of_family_sub W Tw0 A HA).
Set BcompY to be the term restrict_family_to_subspace A WYc.
Set AyOf to be the term λU : set ⇒ Eps_i (λV : set ⇒ V ∈ A ∧ U ⊆ V) of type set → set.
Set VyOf to be the term λU : set ⇒ Eps_i (λV : set ⇒ V ∈ Tw0 ∧ U = V ∩ Y) of type set → set.
Set liftY to be the term λU : set ⇒ (VyOf U) ∩ (AyOf U) of type set → set.
Set BYlift to be the term {liftY U|U ∈ BY}.
Set B to be the term BcompY ∪ BYlift.
We prove the intermediate claim HayOf: ∀U : set, U ∈ BY → (AyOf U) ∈ A ∧ U ⊆ AyOf U.
Let U be given.
Assume HU: U ∈ BY.
We prove the intermediate claim Hex: ∃V : set, V ∈ A ∧ U ⊆ V.
Apply (HBYref U HU) to the current goal.
Let V0 be given.
Assume HV0pair.
Apply HV0pair to the current goal.
Assume HV0AY: V0 ∈ AY.
Assume HUV0: U ⊆ V0.
Apply (ReplE_impred A (λV : set ⇒ V ∩ Y) V0 HV0AY (∃V : set, V ∈ A ∧ U ⊆ V)) to the current goal.
Let V be given.
Assume HV: V ∈ A.
Assume HV0eq: V0 = V ∩ Y.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (HUV0 x HxU).
We prove the intermediate claim HxVcap: x ∈ V ∩ Y.
An exact proof term for the current goal is (mem_eqR x V0 (V ∩ Y) HV0eq HxV0).
An exact proof term for the current goal is (binintersectE1 V Y x HxVcap).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ A ∧ U ⊆ V) Hex).
We prove the intermediate claim HvyOf: ∀U : set, U ∈ BY → (VyOf U) ∈ Tw0 ∧ U = (VyOf U) ∩ Y.
Let U be given.
Assume HU: U ∈ BY.
We prove the intermediate claim HUinTy: U ∈ Ty.
An exact proof term for the current goal is (open_cover_of_members_open Y Ty BY U HBYcov HU).
We prove the intermediate claim HUinSubW: U ∈ subspace_topology W Tw0 Y.
An exact proof term for the current goal is (mem_eqL U (subspace_topology W Tw0 Y) Ty HTwyEq HUinTy).
We prove the intermediate claim Hex: ∃V ∈ Tw0, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE W Tw0 Y U HUinSubW).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ V ∈ Tw0 ∧ U = V ∩ Y) Hex).
We prove the intermediate claim HliftOpen: ∀U : set, U ∈ BY → liftY U ∈ Tw0.
Let U be given.
Assume HU: U ∈ BY.
We prove the intermediate claim HayPack: (AyOf U) ∈ A ∧ U ⊆ AyOf U.
An exact proof term for the current goal is (HayOf U HU).
We prove the intermediate claim HayoA: (AyOf U) ∈ A.
An exact proof term for the current goal is (andEL ((AyOf U) ∈ A) (U ⊆ AyOf U) HayPack).
We prove the intermediate claim HayoTw: (AyOf U) ∈ Tw0.
An exact proof term for the current goal is (HAopen (AyOf U) HayoA).
We prove the intermediate claim HvyPack: (VyOf U) ∈ Tw0 ∧ U = (VyOf U) ∩ Y.
An exact proof term for the current goal is (HvyOf U HU).
We prove the intermediate claim HvyTw: (VyOf U) ∈ Tw0.
An exact proof term for the current goal is (andEL ((VyOf U) ∈ Tw0) (U = (VyOf U) ∩ Y) HvyPack).
An exact proof term for the current goal is (topology_binintersect_closed W Tw0 (VyOf U) (AyOf U) HTw HvyTw HayoTw).
We prove the intermediate claim HBmem: ∀V : set, V ∈ B → V ∈ Tw0.
Let V be given.
Assume HV: V ∈ B.
Apply (binunionE BcompY BYlift V HV (V ∈ Tw0)) to the current goal.
Assume HVc: V ∈ BcompY.
Apply (ReplE_impred A (λU : set ⇒ U ∩ WYc) V HVc (V ∈ Tw0)) to the current goal.
Let U be given.
Assume HU: U ∈ A.
Assume HVe: V = U ∩ WYc.
We prove the intermediate claim HUtw: U ∈ Tw0.
An exact proof term for the current goal is (HAopen U HU).
We prove the intermediate claim HUcap: U ∩ WYc ∈ Tw0.
An exact proof term for the current goal is (topology_binintersect_closed W Tw0 U WYc HTw HUtw HWYopen).
An exact proof term for the current goal is (eq_subst_mem V (U ∩ WYc) Tw0 HVe HUcap).
Assume HVl: V ∈ BYlift.
Apply (ReplE_impred BY (λU : set ⇒ liftY U) V HVl (V ∈ Tw0)) to the current goal.
Let U be given.
Assume HU: U ∈ BY.
Assume HVe: V = liftY U.
We prove the intermediate claim HUt: liftY U ∈ Tw0.
An exact proof term for the current goal is (HliftOpen U HU).
An exact proof term for the current goal is (eq_subst_mem V (liftY U) Tw0 HVe HUt).
We prove the intermediate claim HBsubPow: B ⊆ 𝒫 W.
Let V be given.
Assume HV: V ∈ B.
We prove the intermediate claim HVtw: V ∈ Tw0.
An exact proof term for the current goal is (HBmem V HV).
We prove the intermediate claim HVsubW: V ⊆ W.
An exact proof term for the current goal is (topology_elem_subset W Tw0 V HTw HVtw).
An exact proof term for the current goal is (PowerI W V HVsubW).
We prove the intermediate claim HBcov: W ⊆ ⋃ B.
Let x be given.
Assume HxW: x ∈ W.
Apply (xm (x ∈ Y)) to the current goal.
Assume HxY: x ∈ Y.
We prove the intermediate claim HxUnionBY: x ∈ ⋃ BY.
An exact proof term for the current goal is (open_cover_of_covers Y Ty BY HBYcov x HxY).
Apply (UnionE BY x HxUnionBY) to the current goal.
Let U be given.
Assume HUpair: x ∈ U ∧ U ∈ BY.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ BY) HUpair).
We prove the intermediate claim HU: U ∈ BY.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ BY) HUpair).
We prove the intermediate claim HayPack: (AyOf U) ∈ A ∧ U ⊆ AyOf U.
An exact proof term for the current goal is (HayOf U HU).
We prove the intermediate claim HUsubAyo: U ⊆ AyOf U.
An exact proof term for the current goal is (andER ((AyOf U) ∈ A) (U ⊆ AyOf U) HayPack).
We prove the intermediate claim HxAyo: x ∈ AyOf U.
An exact proof term for the current goal is (HUsubAyo x HxU).
We prove the intermediate claim HvyPack: (VyOf U) ∈ Tw0 ∧ U = (VyOf U) ∩ Y.
An exact proof term for the current goal is (HvyOf U HU).
We prove the intermediate claim HUEq: U = (VyOf U) ∩ Y.
An exact proof term for the current goal is (andER ((VyOf U) ∈ Tw0) (U = (VyOf U) ∩ Y) HvyPack).
We prove the intermediate claim HxVcap: x ∈ (VyOf U) ∩ Y.
An exact proof term for the current goal is (mem_eqR x U ((VyOf U) ∩ Y) HUEq HxU).
We prove the intermediate claim HxVy: x ∈ VyOf U.
An exact proof term for the current goal is (binintersectE1 (VyOf U) Y x HxVcap).
We prove the intermediate claim HxLift: x ∈ liftY U.
An exact proof term for the current goal is (binintersectI (VyOf U) (AyOf U) x HxVy HxAyo).
We prove the intermediate claim HUinBYlift: liftY U ∈ BYlift.
An exact proof term for the current goal is (ReplI BY (λU0 : set ⇒ liftY U0) U HU).
We prove the intermediate claim HUinB: liftY U ∈ B.
An exact proof term for the current goal is (binunionI2 BcompY BYlift (liftY U) HUinBYlift).
An exact proof term for the current goal is (UnionI B x (liftY U) HxLift HUinB).
Assume HxNotY: x ∉ Y.
We prove the intermediate claim HxUnionA: x ∈ ⋃ A.
An exact proof term for the current goal is (open_cover_of_covers W Tw0 A HA x HxW).
Apply (UnionE A x HxUnionA) to the current goal.
Let U be given.
Assume HUpair: x ∈ U ∧ U ∈ A.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ A) HUpair).
We prove the intermediate claim HU: U ∈ A.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ A) HUpair).
We prove the intermediate claim HxWYc: x ∈ WYc.
An exact proof term for the current goal is (setminusI W Y x HxW HxNotY).
We prove the intermediate claim HxUc: x ∈ U ∩ WYc.
An exact proof term for the current goal is (binintersectI U WYc x HxU HxWYc).
We prove the intermediate claim HUcFam: U ∩ WYc ∈ BcompY.
An exact proof term for the current goal is (ReplI A (λU0 : set ⇒ U0 ∩ WYc) U HU).
We prove the intermediate claim HUcB: U ∩ WYc ∈ B.
An exact proof term for the current goal is (binunionI1 BcompY BYlift (U ∩ WYc) HUcFam).
An exact proof term for the current goal is (UnionI B x (U ∩ WYc) HxUc HUcB).
We prove the intermediate claim HBcover: open_cover_of W Tw0 B.
Apply (open_cover_ofI W Tw0 B) to the current goal.
An exact proof term for the current goal is HTw.
An exact proof term for the current goal is HBsubPow.
An exact proof term for the current goal is HBcov.
An exact proof term for the current goal is HBmem.
We prove the intermediate claim HBrefA: refines_cover B A.
Let V be given.
Assume HV: V ∈ B.
Apply (binunionE BcompY BYlift V HV (∃U0 : set, U0 ∈ A ∧ V ⊆ U0)) to the current goal.
Assume HVc: V ∈ BcompY.
Apply (ReplE_impred A (λU : set ⇒ U ∩ WYc) V HVc (∃U0 : set, U0 ∈ A ∧ V ⊆ U0)) to the current goal.
Let U be given.
Assume HU: U ∈ A.
Assume HVe: V = U ∩ WYc.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
Let x be given.
Assume HxV: x ∈ V.
We prove the intermediate claim HxCap: x ∈ U ∩ WYc.
An exact proof term for the current goal is (mem_eqR x V (U ∩ WYc) HVe HxV).
An exact proof term for the current goal is (binintersectE1 U WYc x HxCap).
Assume HVl: V ∈ BYlift.
Apply (ReplE_impred BY (λU : set ⇒ liftY U) V HVl (∃U0 : set, U0 ∈ A ∧ V ⊆ U0)) to the current goal.
Let U be given.
Assume HU: U ∈ BY.
Assume HVe: V = liftY U.
We prove the intermediate claim HayPack: (AyOf U) ∈ A ∧ U ⊆ AyOf U.
An exact proof term for the current goal is (HayOf U HU).
We use (AyOf U) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL ((AyOf U) ∈ A) (U ⊆ AyOf U) HayPack).
Let x be given.
Assume HxV: x ∈ V.
We prove the intermediate claim HxLift: x ∈ liftY U.
An exact proof term for the current goal is (mem_eqR x V (liftY U) HVe HxV).
We prove the intermediate claim HliftDef: liftY U = (VyOf U) ∩ (AyOf U).
Use reflexivity.
We prove the intermediate claim HxCap: x ∈ (VyOf U) ∩ (AyOf U).
An exact proof term for the current goal is (mem_eqR x (liftY U) ((VyOf U) ∩ (AyOf U)) HliftDef HxLift).
An exact proof term for the current goal is (binintersectE2 (VyOf U) (AyOf U) x HxCap).
Set BZ0 to be the term restrict_family_to_subspace B Z.
We prove the intermediate claim HBZ0w: open_cover_of Z (subspace_topology W Tw0 Z) BZ0.
An exact proof term for the current goal is (open_cover_of_restrict_to_subspace W Tw0 B Z HBcover HZsubW).
We prove the intermediate claim HBZ0: open_cover_of Z Tz BZ0.
rewrite the current goal using HTwzEq (from right to left).
An exact proof term for the current goal is HBZ0w.
We prove the intermediate claim HexCZ: ∃CZ : set, open_cover_of Z Tz CZ ∧ refines_cover CZ BZ0 ∧ collection_has_order_at_most_m_plus_one Z CZ n.
An exact proof term for the current goal is (HdimZprop BZ0 HBZ0).
Apply HexCZ to the current goal.
Let CZ be given.
Assume HCZpack: open_cover_of Z Tz CZ ∧ refines_cover CZ BZ0 ∧ collection_has_order_at_most_m_plus_one Z CZ n.
We prove the intermediate claim HCZpair: open_cover_of Z Tz CZ ∧ refines_cover CZ BZ0.
An exact proof term for the current goal is (andEL (open_cover_of Z Tz CZ ∧ refines_cover CZ BZ0) (collection_has_order_at_most_m_plus_one Z CZ n) HCZpack).
We prove the intermediate claim HCZcov: open_cover_of Z Tz CZ.
An exact proof term for the current goal is (andEL (open_cover_of Z Tz CZ) (refines_cover CZ BZ0) HCZpair).
We prove the intermediate claim HCZref: refines_cover CZ BZ0.
An exact proof term for the current goal is (andER (open_cover_of Z Tz CZ) (refines_cover CZ BZ0) HCZpair).
We prove the intermediate claim HCZord: collection_has_order_at_most_m_plus_one Z CZ n.
An exact proof term for the current goal is (andER (open_cover_of Z Tz CZ ∧ refines_cover CZ BZ0) (collection_has_order_at_most_m_plus_one Z CZ n) HCZpack).
Set WZc to be the term W ∖ Z.
We prove the intermediate claim HWZopen: WZc ∈ Tw0.
Set Vz to be the term X ∖ Z.
We prove the intermediate claim HVzopenIn: open_in X Tx Vz.
An exact proof term for the current goal is (open_of_closed_complement X Tx Z HZcl).
We prove the intermediate claim HVzTx: Vz ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx Vz HVzopenIn).
We prove the intermediate claim HVzsubW: (Vz ∩ W) ∈ Tw0.
An exact proof term for the current goal is (subspace_topologyI X Tx W Vz HVzTx).
We prove the intermediate claim HWZeq: WZc = Vz ∩ W.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ WZc.
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (setminusE1 W Z x Hx).
We prove the intermediate claim HxnotZ: x ∉ Z.
An exact proof term for the current goal is (setminusE2 W Z x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HWsubX x HxW).
We prove the intermediate claim HxVz: x ∈ Vz.
An exact proof term for the current goal is (setminusI X Z x HxX HxnotZ).
An exact proof term for the current goal is (binintersectI Vz W x HxVz HxW).
Let x be given.
Assume Hx: x ∈ Vz ∩ W.
We prove the intermediate claim HxVz: x ∈ Vz.
An exact proof term for the current goal is (binintersectE1 Vz W x Hx).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (binintersectE2 Vz W x Hx).
We prove the intermediate claim HxnotZ: x ∉ Z.
An exact proof term for the current goal is (setminusE2 X Z x HxVz).
An exact proof term for the current goal is (setminusI W Z x HxW HxnotZ).
An exact proof term for the current goal is (eq_subst_mem WZc (Vz ∩ W) Tw0 HWZeq HVzsubW).
Set bZ to be the term λU : set ⇒ Eps_i (λb : set ⇒ b ∈ B ∧ U ⊆ b ∩ Z) of type set → set.
We prove the intermediate claim HbZspec: ∀U : set, U ∈ CZ → (bZ U) ∈ B ∧ U ⊆ (bZ U) ∩ Z.
Let U be given.
Assume HU: U ∈ CZ.
We prove the intermediate claim Hex0: ∃V : set, V ∈ BZ0 ∧ U ⊆ V.
An exact proof term for the current goal is (HCZref U HU).
Apply Hex0 to the current goal.
Let V be given.
Assume HVpair: V ∈ BZ0 ∧ U ⊆ V.
We prove the intermediate claim HVBZ0: V ∈ BZ0.
An exact proof term for the current goal is (andEL (V ∈ BZ0) (U ⊆ V) HVpair).
We prove the intermediate claim HUV: U ⊆ V.
An exact proof term for the current goal is (andER (V ∈ BZ0) (U ⊆ V) HVpair).
We prove the intermediate claim Hexb: ∃b0 : set, b0 ∈ B ∧ U ⊆ b0 ∩ Z.
Apply (ReplE_impred B (λb0 : set ⇒ b0 ∩ Z) V HVBZ0 (∃b0 : set, b0 ∈ B ∧ U ⊆ b0 ∩ Z)) to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
Assume HVe: V = b0 ∩ Z.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0B.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HUV x HxU).
An exact proof term for the current goal is (mem_eqR x V (b0 ∩ Z) HVe HxV).
An exact proof term for the current goal is (Eps_i_ex (λb0 : set ⇒ b0 ∈ B ∧ U ⊆ b0 ∩ Z) Hexb).
Set vZ to be the term λU : set ⇒ (ambient_open_of_subspace_open W Tw0 Z U) ∩ (bZ U) of type set → set.
We prove the intermediate claim HvZopen: ∀U : set, U ∈ CZ → (vZ U) ∈ Tw0.
Let U be given.
Assume HU: U ∈ CZ.
We prove the intermediate claim HUinTz: U ∈ Tz.
An exact proof term for the current goal is (open_cover_of_members_open Z Tz CZ U HCZcov HU).
We prove the intermediate claim HUinSubW: U ∈ subspace_topology W Tw0 Z.
An exact proof term for the current goal is (mem_eqL U (subspace_topology W Tw0 Z) Tz HTwzEq HUinTz).
We prove the intermediate claim HAmbPack: (ambient_open_of_subspace_open W Tw0 Z U) ∈ Tw0 ∧ U = (ambient_open_of_subspace_open W Tw0 Z U) ∩ Z.
An exact proof term for the current goal is (ambient_open_of_subspace_open_spec W Tw0 Z U HUinSubW).
We prove the intermediate claim HAmbOpen: (ambient_open_of_subspace_open W Tw0 Z U) ∈ Tw0.
An exact proof term for the current goal is (andEL ((ambient_open_of_subspace_open W Tw0 Z U) ∈ Tw0) (U = (ambient_open_of_subspace_open W Tw0 Z U) ∩ Z) HAmbPack).
We prove the intermediate claim HbZB: (bZ U) ∈ B.
An exact proof term for the current goal is (andEL ((bZ U) ∈ B) (U ⊆ (bZ U) ∩ Z) (HbZspec U HU)).
We prove the intermediate claim HbZOpen: (bZ U) ∈ Tw0.
An exact proof term for the current goal is (HBmem (bZ U) HbZB).
An exact proof term for the current goal is (topology_binintersect_closed W Tw0 (ambient_open_of_subspace_open W Tw0 Z U) (bZ U) HTw HAmbOpen HbZOpen).
Set CZb to be the term λb : set ⇒ {U ∈ CZ|bZ U = b} of type set → set.
Set Zpart to be the term λb : set ⇒ ⋃ {vZ U|U ∈ CZb b} of type set → set.
We prove the intermediate claim HZpartOpen: ∀b : set, b ∈ B → (Zpart b) ∈ Tw0.
Let b be given.
Assume HbB: b ∈ B.
Set UFam to be the term {vZ U|U ∈ CZb b}.
We prove the intermediate claim HUFamSub: UFam ⊆ Tw0.
Let V be given.
Assume HV: V ∈ UFam.
Apply (ReplE_impred (CZb b) (λU : set ⇒ vZ U) V HV (V ∈ Tw0)) to the current goal.
Let U be given.
Assume HU: U ∈ CZb b.
Assume HVe: V = vZ U.
We prove the intermediate claim HUinCZ: U ∈ CZ.
An exact proof term for the current goal is (SepE1 CZ (λU0 : set ⇒ bZ U0 = b) U HU).
rewrite the current goal using HVe (from left to right).
An exact proof term for the current goal is (HvZopen U HUinCZ).
We prove the intermediate claim HUFamPow: UFam ∈ 𝒫 Tw0.
An exact proof term for the current goal is (PowerI Tw0 UFam HUFamSub).
An exact proof term for the current goal is (topology_union_closed_pow W Tw0 UFam HTw HUFamPow).
Set Dfun to be the term λb : set ⇒ (b ∩ WZc) ∪ (Zpart b) of type set → set.
Set D to be the term {Dfun b|b ∈ B}.
We prove the intermediate claim HDfunOpen: ∀b : set, b ∈ B → (Dfun b) ∈ Tw0.
Let b be given.
Assume HbB: b ∈ B.
We prove the intermediate claim HbOpen: b ∈ Tw0.
An exact proof term for the current goal is (HBmem b HbB).
We prove the intermediate claim HbWZcOpen: (b ∩ WZc) ∈ Tw0.
An exact proof term for the current goal is (topology_binintersect_closed W Tw0 b WZc HTw HbOpen HWZopen).
We prove the intermediate claim HZpartOpen0: (Zpart b) ∈ Tw0.
An exact proof term for the current goal is (HZpartOpen b HbB).
An exact proof term for the current goal is (topology_binunion_closed W Tw0 (b ∩ WZc) (Zpart b) HTw HbWZcOpen HZpartOpen0).
We prove the intermediate claim HDmem: ∀U : set, U ∈ D → U ∈ Tw0.
Let U be given.
Assume HU: U ∈ D.
Apply (ReplE_impred B (λb : set ⇒ Dfun b) U HU (U ∈ Tw0)) to the current goal.
Let b be given.
Assume HbB: b ∈ B.
Assume HUeq: U = Dfun b.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (HDfunOpen b HbB).
We prove the intermediate claim HDsubPow: D ⊆ 𝒫 W.
Let U be given.
Assume HU: U ∈ D.
We prove the intermediate claim HUopen: U ∈ Tw0.
An exact proof term for the current goal is (HDmem U HU).
We prove the intermediate claim HUsubW: U ⊆ W.
An exact proof term for the current goal is (topology_elem_subset W Tw0 U HTw HUopen).
An exact proof term for the current goal is (PowerI W U HUsubW).
We prove the intermediate claim HDcov: W ⊆ ⋃ D.
Let x be given.
Assume HxW: x ∈ W.
Apply (xm (x ∈ Z)) to the current goal.
Assume HxZ: x ∈ Z.
We prove the intermediate claim HxInUnionCZ: x ∈ ⋃ CZ.
An exact proof term for the current goal is (open_cover_of_covers Z Tz CZ HCZcov x HxZ).
Apply (UnionE CZ x HxInUnionCZ) to the current goal.
Let U be given.
Assume HUpair: x ∈ U ∧ U ∈ CZ.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ CZ) HUpair).
We prove the intermediate claim HUc: U ∈ CZ.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ CZ) HUpair).
Set b to be the term bZ U.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (U ⊆ b ∩ Z) (HbZspec U HUc)).
We prove the intermediate claim HUsub: U ⊆ b ∩ Z.
An exact proof term for the current goal is (andER (b ∈ B) (U ⊆ b ∩ Z) (HbZspec U HUc)).
We prove the intermediate claim HxBcap: x ∈ b ∩ Z.
An exact proof term for the current goal is (HUsub x HxU).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (binintersectE1 b Z x HxBcap).
We prove the intermediate claim HxZpart: x ∈ Zpart b.
Set UFam to be the term {vZ U0|U0 ∈ CZb b}.
We prove the intermediate claim HUinCZb: U ∈ CZb b.
We prove the intermediate claim HCZbDef: CZb b = {U0 ∈ CZ|bZ U0 = b}.
Use reflexivity.
We prove the intermediate claim HUinSep: U ∈ {U0 ∈ CZ|bZ U0 = b}.
We prove the intermediate claim Hbdef0: b = bZ U.
Use reflexivity.
We prove the intermediate claim Hbdef: bZ U = b.
rewrite the current goal using Hbdef0 (from right to left).
Use reflexivity.
An exact proof term for the current goal is (SepI CZ (λU0 : set ⇒ bZ U0 = b) U HUc Hbdef).
An exact proof term for the current goal is (mem_eqL U (CZb b) {U0 ∈ CZ|bZ U0 = b} HCZbDef HUinSep).
We prove the intermediate claim HvZinUFam: vZ U ∈ UFam.
An exact proof term for the current goal is (ReplI (CZb b) (λU0 : set ⇒ vZ U0) U HUinCZb).
We prove the intermediate claim HUinTz: U ∈ Tz.
An exact proof term for the current goal is (open_cover_of_members_open Z Tz CZ U HCZcov HUc).
We prove the intermediate claim HUinSubW: U ∈ subspace_topology W Tw0 Z.
An exact proof term for the current goal is (mem_eqL U (subspace_topology W Tw0 Z) Tz HTwzEq HUinTz).
We prove the intermediate claim HAmbPack: (ambient_open_of_subspace_open W Tw0 Z U) ∈ Tw0 ∧ U = (ambient_open_of_subspace_open W Tw0 Z U) ∩ Z.
An exact proof term for the current goal is (ambient_open_of_subspace_open_spec W Tw0 Z U HUinSubW).
We prove the intermediate claim HUeq: U = (ambient_open_of_subspace_open W Tw0 Z U) ∩ Z.
An exact proof term for the current goal is (andER ((ambient_open_of_subspace_open W Tw0 Z U) ∈ Tw0) (U = (ambient_open_of_subspace_open W Tw0 Z U) ∩ Z) HAmbPack).
We prove the intermediate claim HxCap2: x ∈ (ambient_open_of_subspace_open W Tw0 Z U) ∩ Z.
An exact proof term for the current goal is (mem_eqR x U ((ambient_open_of_subspace_open W Tw0 Z U) ∩ Z) HUeq HxU).
We prove the intermediate claim HxAmb: x ∈ ambient_open_of_subspace_open W Tw0 Z U.
An exact proof term for the current goal is (binintersectE1 (ambient_open_of_subspace_open W Tw0 Z U) Z x HxCap2).
We prove the intermediate claim HxvZ: x ∈ vZ U.
An exact proof term for the current goal is (binintersectI (ambient_open_of_subspace_open W Tw0 Z U) (bZ U) x HxAmb Hxb).
We prove the intermediate claim HxInUnionUFam: x ∈ ⋃ UFam.
An exact proof term for the current goal is (UnionI UFam x (vZ U) HxvZ HvZinUFam).
An exact proof term for the current goal is HxInUnionUFam.
We prove the intermediate claim HxInDfun: x ∈ Dfun b.
An exact proof term for the current goal is (binunionI2 (b ∩ WZc) (Zpart b) x HxZpart).
We prove the intermediate claim HbInD: Dfun b ∈ D.
An exact proof term for the current goal is (ReplI B (λb0 : set ⇒ Dfun b0) b HbB).
An exact proof term for the current goal is (UnionI D x (Dfun b) HxInDfun HbInD).
Assume HxnotZ: x ∉ Z.
We prove the intermediate claim HxWZc: x ∈ WZc.
An exact proof term for the current goal is (setminusI W Z x HxW HxnotZ).
We prove the intermediate claim HxInUnionB: x ∈ ⋃ B.
An exact proof term for the current goal is (open_cover_of_covers W Tw0 B HBcover x HxW).
Apply (UnionE B x HxInUnionB) to the current goal.
Let b be given.
Assume Hbpair: x ∈ b ∧ b ∈ B.
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ∈ B) Hbpair).
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andER (x ∈ b) (b ∈ B) Hbpair).
We prove the intermediate claim HxCap: x ∈ b ∩ WZc.
An exact proof term for the current goal is (binintersectI b WZc x Hxb HxWZc).
We prove the intermediate claim HxInDfun: x ∈ Dfun b.
An exact proof term for the current goal is (binunionI1 (b ∩ WZc) (Zpart b) x HxCap).
We prove the intermediate claim HbInD: Dfun b ∈ D.
An exact proof term for the current goal is (ReplI B (λb0 : set ⇒ Dfun b0) b HbB).
An exact proof term for the current goal is (UnionI D x (Dfun b) HxInDfun HbInD).
We prove the intermediate claim HDcover: open_cover_of W Tw0 D.
Apply (open_cover_ofI W Tw0 D) to the current goal.
An exact proof term for the current goal is HTw.
An exact proof term for the current goal is HDsubPow.
An exact proof term for the current goal is HDcov.
An exact proof term for the current goal is HDmem.
We prove the intermediate claim HZpartSub: ∀b : set, b ∈ B → (Zpart b) ⊆ b.
Let b be given.
Assume HbB: b ∈ B.
Let x be given.
Assume HxZp: x ∈ Zpart b.
Set UFam to be the term {vZ U0|U0 ∈ CZb b}.
We prove the intermediate claim HZpDef: Zpart b = ⋃ UFam.
Use reflexivity.
We prove the intermediate claim HxUFam: x ∈ ⋃ UFam.
An exact proof term for the current goal is (mem_eqR x (Zpart b) (⋃ UFam) HZpDef HxZp).
Apply (UnionE UFam x HxUFam) to the current goal.
Let V be given.
Assume HVpair: x ∈ V ∧ V ∈ UFam.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (V ∈ UFam) HVpair).
We prove the intermediate claim HVUFam: V ∈ UFam.
An exact proof term for the current goal is (andER (x ∈ V) (V ∈ UFam) HVpair).
Apply (ReplE_impred (CZb b) (λU0 : set ⇒ vZ U0) V HVUFam (x ∈ b)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ CZb b.
Assume HVe: V = vZ U0.
We prove the intermediate claim HxvZ: x ∈ vZ U0.
An exact proof term for the current goal is (mem_eqR x V (vZ U0) HVe HxV).
We prove the intermediate claim HvZDef: vZ U0 = (ambient_open_of_subspace_open W Tw0 Z U0) ∩ (bZ U0).
Use reflexivity.
We prove the intermediate claim HxCap: x ∈ (ambient_open_of_subspace_open W Tw0 Z U0) ∩ (bZ U0).
An exact proof term for the current goal is (mem_eqR x (vZ U0) ((ambient_open_of_subspace_open W Tw0 Z U0) ∩ (bZ U0)) HvZDef HxvZ).
We prove the intermediate claim HxBz: x ∈ bZ U0.
An exact proof term for the current goal is (binintersectE2 (ambient_open_of_subspace_open W Tw0 Z U0) (bZ U0) x HxCap).
We prove the intermediate claim HbZU0: bZ U0 = b.
An exact proof term for the current goal is (SepE2 CZ (λU1 : set ⇒ bZ U1 = b) U0 HU0).
An exact proof term for the current goal is (mem_eqR x (bZ U0) b HbZU0 HxBz).
We prove the intermediate claim HDfunSub: ∀b : set, b ∈ B → (Dfun b) ⊆ b.
Let b be given.
Assume HbB: b ∈ B.
Let x be given.
Assume HxDf: x ∈ Dfun b.
We prove the intermediate claim HDfDef: Dfun b = (b ∩ WZc) ∪ (Zpart b).
Use reflexivity.
We prove the intermediate claim HxUn: x ∈ (b ∩ WZc) ∪ (Zpart b).
An exact proof term for the current goal is (mem_eqR x (Dfun b) ((b ∩ WZc) ∪ (Zpart b)) HDfDef HxDf).
Apply (binunionE (b ∩ WZc) (Zpart b) x HxUn (x ∈ b)) to the current goal.
Assume HxCap: x ∈ b ∩ WZc.
An exact proof term for the current goal is (binintersectE1 b WZc x HxCap).
Assume HxZp: x ∈ Zpart b.
An exact proof term for the current goal is (HZpartSub b HbB x HxZp).
We prove the intermediate claim HDrefB: refines_cover D B.
Let U be given.
Assume HU: U ∈ D.
Apply (ReplE_impred B (λb0 : set ⇒ Dfun b0) U HU (∃V : set, V ∈ B ∧ U ⊆ V)) to the current goal.
Let b be given.
Assume HbB: b ∈ B.
Assume HUeq: U = Dfun b.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxDf: x ∈ Dfun b.
An exact proof term for the current goal is (mem_eqR x U (Dfun b) HUeq HxU).
An exact proof term for the current goal is (HDfunSub b HbB x HxDf).
We prove the intermediate claim HDrefA: refines_cover D A.
An exact proof term for the current goal is (refines_cover_tra A B D HDrefB HBrefA).
We use D to witness the existential quantifier.
We will prove open_cover_of W Tw0 D ∧ refines_cover D A ∧ collection_has_order_at_most_m_plus_one W D n.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HDcover.
An exact proof term for the current goal is HDrefA.
We will prove collection_has_order_at_most_m_plus_one W D n.
We will prove ordinal n ∧ ∀x : set, x ∈ W → cardinality_at_most {U ∈ D|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 HxW: x ∈ W.
We prove the intermediate claim HWdef: W = Y ∪ Z.
Use reflexivity.
We prove the intermediate claim HxYZ: x ∈ Y ∪ Z.
An exact proof term for the current goal is (mem_eqR x W (Y ∪ Z) HWdef HxW).
Apply (binunionE Y Z x HxYZ (cardinality_at_most {U ∈ D|x ∈ U} (ordsucc n))) to the current goal.
Assume HxY: x ∈ Y.
Set n1 to be the term ordsucc n.
We prove the intermediate claim Hn1O: n1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
Set SBY to be the term {U ∈ BY|x ∈ U}.
We prove the intermediate claim HSByCard: cardinality_at_most SBY n1.
We prove the intermediate claim HBYordF: ∀x0 : set, x0 ∈ Y → cardinality_at_most {U ∈ BY|x0 ∈ U} n1.
An exact proof term for the current goal is (andER (ordinal n) (∀x0 : set, x0 ∈ Y → cardinality_at_most {U ∈ BY|x0 ∈ U} n1) HBYord).
An exact proof term for the current goal is (HBYordF x HxY).
Set ImgLift to be the term {liftY U|U ∈ SBY}.
We prove the intermediate claim HImgLiftCard: cardinality_at_most ImgLift n1.
An exact proof term for the current goal is (cardinality_at_most_image_finite SBY n liftY HnO HSByCard).
Set SB to be the term {b ∈ B|x ∈ b}.
We prove the intermediate claim HSBsub: SB ⊆ ImgLift.
Let b be given.
Assume HbSB: b ∈ SB.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ x ∈ b0) b HbSB).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (SepE2 B (λb0 : set ⇒ x ∈ b0) b HbSB).
Apply (binunionE BcompY BYlift b HbB (b ∈ ImgLift)) to the current goal.
Assume HbC: b ∈ BcompY.
Apply FalseE to the current goal.
Apply (ReplE_impred A (λU0 : set ⇒ U0 ∩ WYc) b HbC False) to the current goal.
Let U0 be given.
Assume HU0A: U0 ∈ A.
Assume HbEq: b = U0 ∩ WYc.
We prove the intermediate claim HxbCap: x ∈ U0 ∩ WYc.
An exact proof term for the current goal is (mem_eqR x b (U0 ∩ WYc) HbEq Hxb).
We prove the intermediate claim HxWYc: x ∈ WYc.
An exact proof term for the current goal is (binintersectE2 U0 WYc x HxbCap).
An exact proof term for the current goal is ((setminusE2 W Y x HxWYc) HxY).
Assume HbL: b ∈ BYlift.
Apply (ReplE_impred BY (λU0 : set ⇒ liftY U0) b HbL (b ∈ ImgLift)) to the current goal.
Let U0 be given.
Assume HU0BY: U0 ∈ BY.
Assume HbEq: b = liftY U0.
We prove the intermediate claim HUEq: U0 = (VyOf U0) ∩ Y.
An exact proof term for the current goal is (andER ((VyOf U0) ∈ Tw0) (U0 = (VyOf U0) ∩ Y) (HvyOf U0 HU0BY)).
We prove the intermediate claim HxbLift: x ∈ liftY U0.
An exact proof term for the current goal is (mem_eqR x b (liftY U0) HbEq Hxb).
We prove the intermediate claim HxCap: x ∈ (VyOf U0) ∩ (AyOf U0).
We prove the intermediate claim HliftDef: liftY U0 = (VyOf U0) ∩ (AyOf U0).
Use reflexivity.
An exact proof term for the current goal is (mem_eqR x (liftY U0) ((VyOf U0) ∩ (AyOf U0)) HliftDef HxbLift).
We prove the intermediate claim HxVy: x ∈ VyOf U0.
An exact proof term for the current goal is (binintersectE1 (VyOf U0) (AyOf U0) x HxCap).
We prove the intermediate claim HxU0: x ∈ U0.
We prove the intermediate claim HxCapY: x ∈ (VyOf U0) ∩ Y.
An exact proof term for the current goal is (binintersectI (VyOf U0) Y x HxVy HxY).
An exact proof term for the current goal is (mem_eqL x U0 ((VyOf U0) ∩ Y) HUEq HxCapY).
We prove the intermediate claim HU0SBY: U0 ∈ SBY.
An exact proof term for the current goal is (SepI BY (λU1 : set ⇒ x ∈ U1) U0 HU0BY HxU0).
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (ReplI SBY (λU1 : set ⇒ liftY U1) U0 HU0SBY).
We prove the intermediate claim HSBCard: cardinality_at_most SB n1.
An exact proof term for the current goal is (cardinality_at_most_mono_subset_finite SB ImgLift n1 Hn1O HSBsub HImgLiftCard).
Set ImgD to be the term {Dfun b|b ∈ SB}.
We prove the intermediate claim HImgDCard: cardinality_at_most ImgD n1.
An exact proof term for the current goal is (cardinality_at_most_image_finite SB n Dfun HnO HSBCard).
We prove the intermediate claim HSDsub: {U ∈ D|x ∈ U} ⊆ ImgD.
Let U be given.
Assume HU: U ∈ {U ∈ D|x ∈ U}.
We prove the intermediate claim HUinD: U ∈ D.
An exact proof term for the current goal is (SepE1 D (λU0 : set ⇒ x ∈ U0) U HU).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepE2 D (λU0 : set ⇒ x ∈ U0) U HU).
Apply (ReplE_impred B (λb0 : set ⇒ Dfun b0) U HUinD (U ∈ ImgD)) to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
Assume HUeq: U = Dfun b0.
We prove the intermediate claim HxDf: x ∈ Dfun b0.
An exact proof term for the current goal is (mem_eqR x U (Dfun b0) HUeq HxU).
We prove the intermediate claim HDfSub: Dfun b0 ⊆ b0.
An exact proof term for the current goal is (HDfunSub b0 Hb0B).
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (HDfSub x HxDf).
We prove the intermediate claim Hb0SB: b0 ∈ SB.
An exact proof term for the current goal is (SepI B (λb1 : set ⇒ x ∈ b1) b0 Hb0B Hxb0).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (ReplI SB (λb1 : set ⇒ Dfun b1) b0 Hb0SB).
An exact proof term for the current goal is (cardinality_at_most_mono_subset_finite {U ∈ D|x ∈ U} ImgD n1 Hn1O HSDsub HImgDCard).
Assume HxZ: x ∈ Z.
Set n1 to be the term ordsucc n.
We prove the intermediate claim Hn1O: n1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim HCZordF: ∀x0 : set, x0 ∈ Z → cardinality_at_most {U ∈ CZ|x0 ∈ U} n1.
An exact proof term for the current goal is (andER (ordinal n) (∀x0 : set, x0 ∈ Z → cardinality_at_most {U ∈ CZ|x0 ∈ U} n1) HCZord).
Set SCZ to be the term {U ∈ CZ|x ∈ U}.
We prove the intermediate claim HSCZCard: cardinality_at_most SCZ n1.
An exact proof term for the current goal is (HCZordF x HxZ).
Set fZ to be the term λU0 : set ⇒ Dfun (bZ U0) of type set → set.
Set ImgZ to be the term {fZ U0|U0 ∈ SCZ}.
We prove the intermediate claim HImgZCard: cardinality_at_most ImgZ n1.
An exact proof term for the current goal is (cardinality_at_most_image_finite SCZ n fZ HnO HSCZCard).
We prove the intermediate claim HSDsub: {U ∈ D|x ∈ U} ⊆ ImgZ.
Let U be given.
Assume HU: U ∈ {U ∈ D|x ∈ U}.
We prove the intermediate claim HUinD: U ∈ D.
An exact proof term for the current goal is (SepE1 D (λU0 : set ⇒ x ∈ U0) U HU).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepE2 D (λU0 : set ⇒ x ∈ U0) U HU).
Apply (ReplE_impred B (λb0 : set ⇒ Dfun b0) U HUinD (U ∈ ImgZ)) to the current goal.
Let b0 be given.
Assume Hb0B: b0 ∈ B.
Assume HUeq: U = Dfun b0.
We prove the intermediate claim HxDf: x ∈ Dfun b0.
An exact proof term for the current goal is (mem_eqR x U (Dfun b0) HUeq HxU).
We prove the intermediate claim HDfDef: Dfun b0 = (b0 ∩ WZc) ∪ (Zpart b0).
Use reflexivity.
We prove the intermediate claim HxUn: x ∈ (b0 ∩ WZc) ∪ (Zpart b0).
An exact proof term for the current goal is (mem_eqR x (Dfun b0) ((b0 ∩ WZc) ∪ (Zpart b0)) HDfDef HxDf).
Apply (binunionE (b0 ∩ WZc) (Zpart b0) x HxUn (U ∈ ImgZ)) to the current goal.
Assume HxCap: x ∈ b0 ∩ WZc.
Apply FalseE to the current goal.
We prove the intermediate claim HxWZc: x ∈ WZc.
An exact proof term for the current goal is (binintersectE2 b0 WZc x HxCap).
An exact proof term for the current goal is ((setminusE2 W Z x HxWZc) HxZ).
Assume HxZp: x ∈ Zpart b0.
Set UFam to be the term {vZ U1|U1 ∈ CZb b0}.
We prove the intermediate claim HZpDef: Zpart b0 = ⋃ UFam.
Use reflexivity.
We prove the intermediate claim HxUFam: x ∈ ⋃ UFam.
An exact proof term for the current goal is (mem_eqR x (Zpart b0) (⋃ UFam) HZpDef HxZp).
Apply (UnionE UFam x HxUFam) to the current goal.
Let V be given.
Assume HVpair: x ∈ V ∧ V ∈ UFam.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (V ∈ UFam) HVpair).
We prove the intermediate claim HVUFam: V ∈ UFam.
An exact proof term for the current goal is (andER (x ∈ V) (V ∈ UFam) HVpair).
Apply (ReplE_impred (CZb b0) (λU1 : set ⇒ vZ U1) V HVUFam (U ∈ ImgZ)) to the current goal.
Let U1 be given.
Assume HU1: U1 ∈ CZb b0.
Assume HVe: V = vZ U1.
We prove the intermediate claim HbZU1: bZ U1 = b0.
An exact proof term for the current goal is (SepE2 CZ (λU2 : set ⇒ bZ U2 = b0) U1 HU1).
We prove the intermediate claim HU1CZ: U1 ∈ CZ.
An exact proof term for the current goal is (SepE1 CZ (λU2 : set ⇒ bZ U2 = b0) U1 HU1).
We prove the intermediate claim HxvZ: x ∈ vZ U1.
An exact proof term for the current goal is (mem_eqR x V (vZ U1) HVe HxV).
We prove the intermediate claim HvZDef: vZ U1 = (ambient_open_of_subspace_open W Tw0 Z U1) ∩ (bZ U1).
Use reflexivity.
We prove the intermediate claim HxCap2: x ∈ (ambient_open_of_subspace_open W Tw0 Z U1) ∩ (bZ U1).
An exact proof term for the current goal is (mem_eqR x (vZ U1) ((ambient_open_of_subspace_open W Tw0 Z U1) ∩ (bZ U1)) HvZDef HxvZ).
We prove the intermediate claim HxAmb: x ∈ ambient_open_of_subspace_open W Tw0 Z U1.
An exact proof term for the current goal is (binintersectE1 (ambient_open_of_subspace_open W Tw0 Z U1) (bZ U1) x HxCap2).
We prove the intermediate claim HU1inTz: U1 ∈ Tz.
An exact proof term for the current goal is (open_cover_of_members_open Z Tz CZ U1 HCZcov HU1CZ).
We prove the intermediate claim HU1inSubW: U1 ∈ subspace_topology W Tw0 Z.
An exact proof term for the current goal is (mem_eqL U1 (subspace_topology W Tw0 Z) Tz HTwzEq HU1inTz).
We prove the intermediate claim HAmbPack: (ambient_open_of_subspace_open W Tw0 Z U1) ∈ Tw0 ∧ U1 = (ambient_open_of_subspace_open W Tw0 Z U1) ∩ Z.
An exact proof term for the current goal is (ambient_open_of_subspace_open_spec W Tw0 Z U1 HU1inSubW).
We prove the intermediate claim HU1eq: U1 = (ambient_open_of_subspace_open W Tw0 Z U1) ∩ Z.
An exact proof term for the current goal is (andER ((ambient_open_of_subspace_open W Tw0 Z U1) ∈ Tw0) (U1 = (ambient_open_of_subspace_open W Tw0 Z U1) ∩ Z) HAmbPack).
We prove the intermediate claim HxCapZ: x ∈ (ambient_open_of_subspace_open W Tw0 Z U1) ∩ Z.
An exact proof term for the current goal is (binintersectI (ambient_open_of_subspace_open W Tw0 Z U1) Z x HxAmb HxZ).
We prove the intermediate claim HxU1: x ∈ U1.
An exact proof term for the current goal is (mem_eqL x U1 ((ambient_open_of_subspace_open W Tw0 Z U1) ∩ Z) HU1eq HxCapZ).
We prove the intermediate claim HU1SCZ: U1 ∈ SCZ.
An exact proof term for the current goal is (SepI CZ (λU2 : set ⇒ x ∈ U2) U1 HU1CZ HxU1).
We prove the intermediate claim HUeq2: U = fZ U1.
rewrite the current goal using HUeq (from left to right).
rewrite the current goal using HbZU1 (from right to left).
Use reflexivity.
rewrite the current goal using HUeq2 (from left to right).
An exact proof term for the current goal is (ReplI SCZ (λU2 : set ⇒ fZ U2) U1 HU1SCZ).
An exact proof term for the current goal is (cardinality_at_most_mono_subset_finite {U ∈ D|x ∈ U} ImgZ n1 Hn1O HSDsub HImgZCard).
∎