Let UY be given.

Assume HUY: open_cover Y Ty UY.

We will prove ∃VY : set, open_cover Y Ty VY ∧ locally_finite_family Y Ty VY ∧ refine_of VY UY.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U) Hpara).

We prove the intermediate claim HYpkg: Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U.

An exact proof term for the current goal is (closed_in_package X Tx Y HYcl).

We prove the intermediate claim HYsubX: Y ⊆ X.

An exact proof term for the current goal is (andEL (Y ⊆ X) (∃U ∈ Tx, Y = X ∖ U) HYpkg).

We prove the intermediate claim HTy: topology_on Y Ty.

An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsubX).

We prove the intermediate claim HUYop: ∀u : set, u ∈ UY → u ∈ Ty.

An exact proof term for the current goal is (andEL (∀u : set, u ∈ UY → u ∈ Ty) (covers Y UY) HUY).

We prove the intermediate claim HUYcov: covers Y UY.

An exact proof term for the current goal is (andER (∀u : set, u ∈ UY → u ∈ Ty) (covers Y UY) HUY).

Set U0 to be the term {V ∈ Tx|∃u ∈ UY, u = V ∩ Y}.

We prove the intermediate claim HXYopen: X ∖ Y ∈ Tx.

We prove the intermediate claim Hop: open_in X Tx (X ∖ Y).

An exact proof term for the current goal is (open_of_closed_complement X Tx Y HYcl).

An exact proof term for the current goal is (andER (topology_on X Tx) ((X ∖ Y) ∈ Tx) Hop).

Set UX to be the term U0 ∪ {X ∖ Y}.

We prove the intermediate claim HUXopen: ∀u : set, u ∈ UX → u ∈ Tx.

Let u be given.

Assume HuUX: u ∈ UX.

Apply (binunionE U0 {X ∖ Y} u HuUX) to the current goal.

Assume HuU0: u ∈ U0.

An exact proof term for the current goal is (SepE1 Tx (λV : set ⇒ ∃u0 ∈ UY, u0 = V ∩ Y) u HuU0).

Assume HuS: u ∈ {X ∖ Y}.

We prove the intermediate claim HuEq: u = X ∖ Y.

An exact proof term for the current goal is (SingE (X ∖ Y) u HuS).

rewrite the current goal using HuEq (from left to right).

An exact proof term for the current goal is HXYopen.

We prove the intermediate claim HUXcov: covers X UX.

Let x be given.

Assume HxX: x ∈ X.

Apply (xm (x ∈ Y)) to the current goal.

Assume HxY: x ∈ Y.

We prove the intermediate claim HcovYx: ∃u : set, u ∈ UY ∧ x ∈ u.

An exact proof term for the current goal is (HUYcov x HxY).

Apply HcovYx to the current goal.

Let u be given.

Assume Hu: u ∈ UY ∧ x ∈ u.

We prove the intermediate claim HuUY: u ∈ UY.

An exact proof term for the current goal is (andEL (u ∈ UY) (x ∈ u) Hu).

We prove the intermediate claim Hxu: x ∈ u.

An exact proof term for the current goal is (andER (u ∈ UY) (x ∈ u) Hu).

We prove the intermediate claim HuTy: u ∈ Ty.

An exact proof term for the current goal is (HUYop u HuUY).

We prove the intermediate claim HexV: ∃V ∈ Tx, u = V ∩ Y.

An exact proof term for the current goal is (subspace_topologyE X Tx Y u HuTy).

Apply HexV to the current goal.

Let V be given.

Assume HV: V ∈ Tx ∧ u = V ∩ Y.

We prove the intermediate claim HVTx: V ∈ Tx.

An exact proof term for the current goal is (andEL (V ∈ Tx) (u = V ∩ Y) HV).

We prove the intermediate claim HuEq: u = V ∩ Y.

An exact proof term for the current goal is (andER (V ∈ Tx) (u = V ∩ Y) HV).

We use V to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HVU0: V ∈ U0.

Apply (SepI Tx (λW : set ⇒ ∃u0 ∈ UY, u0 = W ∩ Y) V HVTx) to the current goal.

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HuUY.

An exact proof term for the current goal is HuEq.

An exact proof term for the current goal is (binunionI1 U0 {X ∖ Y} V HVU0).

We prove the intermediate claim HxVY: x ∈ V ∩ Y.

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 (binintersectE1 V Y x HxVY).

Assume HxNotY: ¬ (x ∈ Y).

We use (X ∖ Y) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (binunionI2 U0 {X ∖ Y} (X ∖ Y) (SingI (X ∖ Y))).

An exact proof term for the current goal is (setminusI X Y x HxX HxNotY).

We prove the intermediate claim HUX: open_cover X Tx UX.

We will prove (∀u : set, u ∈ UX → u ∈ Tx) ∧ covers X UX.

Apply andI to the current goal.

An exact proof term for the current goal is HUXopen.

An exact proof term for the current goal is HUXcov.

We prove the intermediate claim HparaFor: ∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U) Hpara).

We prove the intermediate claim HexVX: ∃VX : set, open_cover X Tx VX ∧ locally_finite_family X Tx VX ∧ refine_of VX UX.

An exact proof term for the current goal is (HparaFor UX HUX).

Apply HexVX to the current goal.

Let VX be given.

Assume HVX: open_cover X Tx VX ∧ locally_finite_family X Tx VX ∧ refine_of VX UX.

We prove the intermediate claim HVXab: open_cover X Tx VX ∧ locally_finite_family X Tx VX.

An exact proof term for the current goal is (andEL (open_cover X Tx VX ∧ locally_finite_family X Tx VX) (refine_of VX UX) HVX).

We prove the intermediate claim HrefVX: refine_of VX UX.

An exact proof term for the current goal is (andER (open_cover X Tx VX ∧ locally_finite_family X Tx VX) (refine_of VX UX) HVX).

We prove the intermediate claim HVXcover: open_cover X Tx VX.

An exact proof term for the current goal is (andEL (open_cover X Tx VX) (locally_finite_family X Tx VX) HVXab).

We prove the intermediate claim HLFVX: locally_finite_family X Tx VX.

An exact proof term for the current goal is (andER (open_cover X Tx VX) (locally_finite_family X Tx VX) HVXab).

We prove the intermediate claim HVXop: ∀v : set, v ∈ VX → v ∈ Tx.

An exact proof term for the current goal is (andEL (∀v : set, v ∈ VX → v ∈ Tx) (covers X VX) HVXcover).

We prove the intermediate claim HVXcov: covers X VX.

An exact proof term for the current goal is (andER (∀v : set, v ∈ VX → v ∈ Tx) (covers X VX) HVXcover).

Set VY to be the term {v ∩ Y|v ∈ VX, v ∩ Y ≠ Empty}.

We prove the intermediate claim HVYopen: ∀w : set, w ∈ VY → w ∈ Ty.

Let w be given.

Assume Hw: w ∈ VY.

Apply (ReplSepE_impred VX (λv : set ⇒ v ∩ Y ≠ Empty) (λv : set ⇒ v ∩ Y) w Hw (w ∈ Ty)) to the current goal.

Let v be given.

Assume HvVX: v ∈ VX.

Assume HvNon: v ∩ Y ≠ Empty.

Assume HwEq: w = v ∩ Y.

We prove the intermediate claim HvTx: v ∈ Tx.

An exact proof term for the current goal is (HVXop v HvVX).

We prove the intermediate claim Hsub: v ∩ Y ∈ Ty.

An exact proof term for the current goal is (subspace_topologyI X Tx Y v HvTx).

rewrite the current goal using HwEq (from left to right).

An exact proof term for the current goal is Hsub.

We prove the intermediate claim HVYcov: covers Y VY.

Let y be given.

Assume HyY: y ∈ Y.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HYsubX y HyY).

We prove the intermediate claim Hexv: ∃v : set, v ∈ VX ∧ y ∈ v.

An exact proof term for the current goal is (HVXcov y HyX).

Apply Hexv to the current goal.

Let v be given.

Assume Hv: v ∈ VX ∧ y ∈ v.

We prove the intermediate claim HvVX: v ∈ VX.

An exact proof term for the current goal is (andEL (v ∈ VX) (y ∈ v) Hv).

We prove the intermediate claim Hyv: y ∈ v.

An exact proof term for the current goal is (andER (v ∈ VX) (y ∈ v) Hv).

Set w to be the term v ∩ Y.

We use w to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplSepI VX (λt : set ⇒ t ∩ Y ≠ Empty) (λt : set ⇒ t ∩ Y) v HvVX (elem_implies_nonempty (v ∩ Y) y (binintersectI v Y y Hyv HyY))).

An exact proof term for the current goal is (binintersectI v Y y Hyv HyY).

We prove the intermediate claim HVY: open_cover Y Ty VY.

We will prove (∀w : set, w ∈ VY → w ∈ Ty) ∧ covers Y VY.

Apply andI to the current goal.

An exact proof term for the current goal is HVYopen.

An exact proof term for the current goal is HVYcov.

We prove the intermediate claim HrefVY: refine_of VY UY.

Let w be given.

Assume Hw: w ∈ VY.

Apply (ReplSepE_impred VX (λv : set ⇒ v ∩ Y ≠ Empty) (λv : set ⇒ v ∩ Y) w Hw (∃u : set, u ∈ UY ∧ w ⊆ u)) to the current goal.

Let v be given.

Assume HvVX: v ∈ VX.

Assume HvNon: v ∩ Y ≠ Empty.

Assume HwEq: w = v ∩ Y.

We prove the intermediate claim Hexu: ∃u : set, u ∈ UX ∧ v ⊆ u.

An exact proof term for the current goal is (HrefVX v HvVX).

Apply Hexu to the current goal.

Let u be given.

Assume Hu: u ∈ UX ∧ v ⊆ u.

We prove the intermediate claim HuUX: u ∈ UX.

An exact proof term for the current goal is (andEL (u ∈ UX) (v ⊆ u) Hu).

We prove the intermediate claim HvSubu: v ⊆ u.

An exact proof term for the current goal is (andER (u ∈ UX) (v ⊆ u) Hu).

Apply (binunionE U0 {X ∖ Y} u HuUX) to the current goal.

Assume HuU0: u ∈ U0.

We prove the intermediate claim Hexu0: ∃u0 ∈ UY, u0 = u ∩ Y.

An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ ∃u0 ∈ UY, u0 = V0 ∩ Y) u HuU0).

Apply Hexu0 to the current goal.

Let u0 be given.

Assume Hu0: u0 ∈ UY ∧ u0 = u ∩ Y.

We prove the intermediate claim Hu0UY: u0 ∈ UY.

An exact proof term for the current goal is (andEL (u0 ∈ UY) (u0 = u ∩ Y) Hu0).

We prove the intermediate claim Hu0Eq: u0 = u ∩ Y.

An exact proof term for the current goal is (andER (u0 ∈ UY) (u0 = u ∩ Y) Hu0).

We use u0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hu0UY.

Let z be given.

Assume Hz: z ∈ w.

We will prove z ∈ u0.

We prove the intermediate claim HzvY: z ∈ v ∩ Y.

rewrite the current goal using HwEq (from right to left).

An exact proof term for the current goal is Hz.

We prove the intermediate claim Hzv: z ∈ v.

An exact proof term for the current goal is (binintersectE1 v Y z HzvY).

We prove the intermediate claim HzY: z ∈ Y.

An exact proof term for the current goal is (binintersectE2 v Y z HzvY).

We prove the intermediate claim Hzu: z ∈ u.

An exact proof term for the current goal is (HvSubu z Hzv).

We prove the intermediate claim HzuY: z ∈ u ∩ Y.

An exact proof term for the current goal is (binintersectI u Y z Hzu HzY).

rewrite the current goal using Hu0Eq (from left to right).

An exact proof term for the current goal is HzuY.

Assume HuComp: u ∈ {X ∖ Y}.

We prove the intermediate claim HuEq: u = X ∖ Y.

An exact proof term for the current goal is (SingE (X ∖ Y) u HuComp).

Apply FalseE to the current goal.

We prove the intermediate claim HwNon: w ≠ Empty.

rewrite the current goal using HwEq (from left to right).

An exact proof term for the current goal is HvNon.

We prove the intermediate claim Hzex: ∃z : set, z ∈ w.

An exact proof term for the current goal is (nonempty_has_element w HwNon).

Apply Hzex to the current goal.

Let z be given.

Assume Hz: z ∈ w.

We prove the intermediate claim HzvY: z ∈ v ∩ Y.

rewrite the current goal using HwEq (from right to left).

An exact proof term for the current goal is Hz.

We prove the intermediate claim Hzv: z ∈ v.

An exact proof term for the current goal is (binintersectE1 v Y z HzvY).

We prove the intermediate claim HzY: z ∈ Y.

An exact proof term for the current goal is (binintersectE2 v Y z HzvY).

We prove the intermediate claim Hzu: z ∈ u.

An exact proof term for the current goal is (HvSubu z Hzv).

We prove the intermediate claim HzuXY: z ∈ X ∖ Y.

rewrite the current goal using HuEq (from right to left).

An exact proof term for the current goal is Hzu.

We prove the intermediate claim HzNotY: z ∉ Y.

An exact proof term for the current goal is (setminusE2 X Y z HzuXY).

An exact proof term for the current goal is (HzNotY HzY).

We prove the intermediate claim HLFVY: locally_finite_family Y Ty VY.

We will prove topology_on Y Ty ∧ ∀y : set, y ∈ Y → ∃N : set, N ∈ Ty ∧ y ∈ N ∧ ∃S : set, finite S ∧ S ⊆ VY ∧ ∀A : set, A ∈ VY → A ∩ N ≠ Empty → A ∈ S.

Apply andI to the current goal.

An exact proof term for the current goal is HTy.

Let y be given.

Assume HyY: y ∈ Y.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HYsubX y HyY).

We prove the intermediate claim HLFpkg: ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S) HLFVX).

We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ y ∈ N ∧ ∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S.

An exact proof term for the current goal is (HLFpkg y HyX).

Apply HexN to the current goal.

Let N be given.

Assume HN: N ∈ Tx ∧ y ∈ N ∧ ∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S.

We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S.

An exact proof term for the current goal is (andER (N ∈ Tx ∧ y ∈ N) (∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S) HN).

We prove the intermediate claim HNy: N ∈ Tx ∧ y ∈ N.

An exact proof term for the current goal is (andEL (N ∈ Tx ∧ y ∈ N) (∃S : set, finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S) HN).

We prove the intermediate claim HNTx: N ∈ Tx.

An exact proof term for the current goal is (andEL (N ∈ Tx) (y ∈ N) HNy).

We prove the intermediate claim HyN: y ∈ N.

An exact proof term for the current goal is (andER (N ∈ Tx) (y ∈ N) HNy).

Set NY to be the term N ∩ Y.

We prove the intermediate claim HNYTy: NY ∈ Ty.

An exact proof term for the current goal is (subspace_topologyI X Tx Y N HNTx).

We prove the intermediate claim HyNY: y ∈ NY.

An exact proof term for the current goal is (binintersectI N Y y HyN HyY).

We use NY to witness the existential quantifier.

Apply andI to the current goal.

We will prove NY ∈ Ty ∧ y ∈ NY.

Apply andI to the current goal.

An exact proof term for the current goal is HNYTy.

An exact proof term for the current goal is HyNY.

Apply HexS to the current goal.

Let S be given.

Assume HS: finite S ∧ S ⊆ VX ∧ ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S.

We prove the intermediate claim HS1: finite S ∧ S ⊆ VX.

An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ VX) (∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S) HS).

We prove the intermediate claim HSprop: ∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S.

An exact proof term for the current goal is (andER (finite S ∧ S ⊆ VX) (∀A : set, A ∈ VX → A ∩ N ≠ Empty → A ∈ S) HS).

We prove the intermediate claim HSfin: finite S.

An exact proof term for the current goal is (andEL (finite S) (S ⊆ VX) HS1).

We prove the intermediate claim HSsubVX: S ⊆ VX.

An exact proof term for the current goal is (andER (finite S) (S ⊆ VX) HS1).

Set SY to be the term {v ∩ Y|v ∈ S, v ∩ Y ≠ Empty}.

We use SY to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HSimgfin: finite {t ∩ Y|t ∈ S}.

An exact proof term for the current goal is (Repl_finite (λt : set ⇒ t ∩ Y) S HSfin).

We prove the intermediate claim HSYsub: SY ⊆ {t ∩ Y|t ∈ S}.

Let w be given.

Assume HwSY: w ∈ SY.

Apply (ReplSepE_impred S (λt : set ⇒ t ∩ Y ≠ Empty) (λt : set ⇒ t ∩ Y) w HwSY (w ∈ {t ∩ Y|t ∈ S})) to the current goal.

Let t be given.

Assume HtS: t ∈ S.

Assume HtNon: t ∩ Y ≠ Empty.

Assume HwEq: w = t ∩ Y.

rewrite the current goal using HwEq (from left to right).

An exact proof term for the current goal is (ReplI S (λt0 : set ⇒ t0 ∩ Y) t HtS).

An exact proof term for the current goal is (Subq_finite {t ∩ Y|t ∈ S} HSimgfin SY HSYsub).

Let w be given.

Assume HwSY: w ∈ SY.

Apply (ReplSepE_impred S (λt : set ⇒ t ∩ Y ≠ Empty) (λt : set ⇒ t ∩ Y) w HwSY (w ∈ VY)) to the current goal.

Let t be given.

Assume HtS: t ∈ S.

Assume HtNon: t ∩ Y ≠ Empty.

Assume HwEq: w = t ∩ Y.

We prove the intermediate claim HtVX: t ∈ VX.

An exact proof term for the current goal is (HSsubVX t HtS).

rewrite the current goal using HwEq (from left to right).

An exact proof term for the current goal is (ReplSepI VX (λv0 : set ⇒ v0 ∩ Y ≠ Empty) (λv0 : set ⇒ v0 ∩ Y) t HtVX HtNon).

Let A be given.

Assume HA: A ∈ VY.

Assume HAnN: A ∩ NY ≠ Empty.

Apply (ReplSepE_impred VX (λv0 : set ⇒ v0 ∩ Y ≠ Empty) (λv0 : set ⇒ v0 ∩ Y) A HA (A ∈ SY)) to the current goal.

Let v0 be given.

Assume Hv0VX: v0 ∈ VX.

Assume Hv0Non: v0 ∩ Y ≠ Empty.

Assume HAeq: A = v0 ∩ Y.

We prove the intermediate claim Hexz: ∃z : set, z ∈ A ∩ NY.

An exact proof term for the current goal is (nonempty_has_element (A ∩ NY) HAnN).

Apply Hexz to the current goal.

Let z be given.

Assume Hz: z ∈ A ∩ NY.

We prove the intermediate claim HzA: z ∈ A.

An exact proof term for the current goal is (binintersectE1 A NY z Hz).

We prove the intermediate claim HzNY: z ∈ NY.

An exact proof term for the current goal is (binintersectE2 A NY z Hz).

We prove the intermediate claim Hzv0Y: z ∈ v0 ∩ Y.

rewrite the current goal using HAeq (from right to left).

An exact proof term for the current goal is HzA.

We prove the intermediate claim Hzv0: z ∈ v0.

An exact proof term for the current goal is (binintersectE1 v0 Y z Hzv0Y).

We prove the intermediate claim HzN: z ∈ N.

An exact proof term for the current goal is (binintersectE1 N Y z HzNY).

We prove the intermediate claim Hzv0N: z ∈ v0 ∩ N.

An exact proof term for the current goal is (binintersectI v0 N z Hzv0 HzN).

We prove the intermediate claim Hv0N: v0 ∩ N ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty (v0 ∩ N) z Hzv0N).

We prove the intermediate claim Hv0S: v0 ∈ S.

An exact proof term for the current goal is (HSprop v0 Hv0VX Hv0N).

rewrite the current goal using HAeq (from left to right).

An exact proof term for the current goal is (ReplSepI S (λt1 : set ⇒ t1 ∩ Y ≠ Empty) (λt1 : set ⇒ t1 ∩ Y) v0 Hv0S Hv0Non).

We use VY to witness the existential quantifier.

We will prove (open_cover Y Ty VY ∧ locally_finite_family Y Ty VY) ∧ refine_of VY UY.

Apply andI to the current goal.

An exact proof term for the current goal is HVY.

An exact proof term for the current goal is HLFVY.

An exact proof term for the current goal is HrefVY.