Let X, Tx and Y be given.
Assume HB: Baire_space X Tx.
Assume HYopen: open_in X Tx Y.
We will prove Baire_space Y (subspace_topology X Tx Y).
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, U ⊆ Tx → countable_set U → (∀u : set, u ∈ U → u ∈ Tx ∧ dense_in u X Tx) → dense_in (intersection_over_family X U) X Tx) HB).
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (open_in_subset X Tx Y HYopen).
We prove the intermediate claim HYinTx: Y ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx Y HYopen).
We prove the intermediate claim HTy: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).
We prove the intermediate claim HBcX: Baire_space_closed X Tx.
An exact proof term for the current goal is (Baire_space_imp_closed X Tx HB).
We prove the intermediate claim HpropX: ∀Fam0 : set, countable_set Fam0 → (∀A0 : set, A0 ∈ Fam0 → closed_in X Tx A0 ∧ interior_of X Tx A0 = Empty) → interior_of X Tx (⋃ Fam0) = Empty.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀Fam0 : set, countable_set Fam0 → (∀A0 : set, A0 ∈ Fam0 → closed_in X Tx A0 ∧ interior_of X Tx A0 = Empty) → interior_of X Tx (⋃ Fam0) = Empty) HBcX).
We prove the intermediate claim HBcY: Baire_space_closed Y (subspace_topology X Tx Y).
We will prove topology_on Y (subspace_topology X Tx Y) ∧ ∀Fam : set, countable_set Fam → (∀A : set, A ∈ Fam → closed_in Y (subspace_topology X Tx Y) A ∧ interior_of Y (subspace_topology X Tx Y) A = Empty) → interior_of Y (subspace_topology X Tx Y) (⋃ Fam) = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is HTy.
Let Fam be given.
Assume Hcount: countable_set Fam.
Assume HFam: ∀A : set, A ∈ Fam → closed_in Y (subspace_topology X Tx Y) A ∧ interior_of Y (subspace_topology X Tx Y) A = Empty.
We will prove interior_of Y (subspace_topology X Tx Y) (⋃ Fam) = Empty.
Set FamX to be the term {closure_of X Tx A|A ∈ Fam}.
We prove the intermediate claim HcountX: countable_set FamX.
An exact proof term for the current goal is (countable_image Fam Hcount (λA0 : set ⇒ closure_of X Tx A0)).
We prove the intermediate claim HFamX: ∀C : set, C ∈ FamX → closed_in X Tx C ∧ interior_of X Tx C = Empty.
Let C be given.
Assume HC: C ∈ FamX.
We prove the intermediate claim HexA: ∃A : set, A ∈ Fam ∧ C = closure_of X Tx A.
An exact proof term for the current goal is (ReplE Fam (λA0 : set ⇒ closure_of X Tx A0) C HC).
Apply HexA to the current goal.
Let A be given.
Assume HA: A ∈ Fam ∧ C = closure_of X Tx A.
We prove the intermediate claim HAin: A ∈ Fam.
An exact proof term for the current goal is (andEL (A ∈ Fam) (C = closure_of X Tx A) HA).
We prove the intermediate claim HeqC: C = closure_of X Tx A.
An exact proof term for the current goal is (andER (A ∈ Fam) (C = closure_of X Tx A) HA).
We prove the intermediate claim HApack: closed_in Y (subspace_topology X Tx Y) A ∧ interior_of Y (subspace_topology X Tx Y) A = Empty.
An exact proof term for the current goal is (HFam A HAin).
We prove the intermediate claim HclosedY: closed_in Y (subspace_topology X Tx Y) A.
An exact proof term for the current goal is (andEL (closed_in Y (subspace_topology X Tx Y) A) (interior_of Y (subspace_topology X Tx Y) A = Empty) HApack).
We prove the intermediate claim HintY: interior_of Y (subspace_topology X Tx Y) A = Empty.
An exact proof term for the current goal is (andER (closed_in Y (subspace_topology X Tx Y) A) (interior_of Y (subspace_topology X Tx Y) A = Empty) HApack).
We prove the intermediate claim HAsubY: A ⊆ Y.
An exact proof term for the current goal is (closed_in_subset Y (subspace_topology X Tx Y) A HclosedY).
We prove the intermediate claim HAsubX: A ⊆ X.
Let a be given.
Assume Ha: a ∈ A.
An exact proof term for the current goal is (HYsub a (HAsubY a Ha)).
We prove the intermediate claim HclosedX: closed_in X Tx (closure_of X Tx A).
An exact proof term for the current goal is (closure_is_closed X Tx A HTx HAsubX).
We prove the intermediate claim HintX: interior_of X Tx (closure_of X Tx A) = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ interior_of X Tx (closure_of X Tx A).
We will prove x ∈ Empty.
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ⊆ closure_of X Tx A.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ closure_of X Tx A) x Hx).
Apply HexU to the current goal.
Let U be given.
Assume HU: U ∈ Tx ∧ x ∈ U ∧ U ⊆ closure_of X Tx A.
We prove the intermediate claim HU12: U ∈ Tx ∧ x ∈ U.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (U ⊆ closure_of X Tx A) HU).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HU12).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HU12).
We prove the intermediate claim HUsub: U ⊆ closure_of X Tx A.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (U ⊆ closure_of X Tx A) HU).
We prove the intermediate claim HxclA: x ∈ closure_of X Tx A.
An exact proof term for the current goal is (HUsub x HxU).
We prove the intermediate claim Hclcond: ∀V : set, V ∈ Tx → x ∈ V → V ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀V : set, V ∈ Tx → x0 ∈ V → V ∩ A ≠ Empty) x HxclA).
We prove the intermediate claim HUAne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hclcond U HUinTx HxU).
We prove the intermediate claim Hexy: ∃y : set, y ∈ U ∩ A.
An exact proof term for the current goal is (nonempty_has_element (U ∩ A) HUAne).
Apply Hexy to the current goal.
Let y be given.
Assume HyUA: y ∈ U ∩ A.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y HyUA).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y HyUA).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (HAsubY y HyA).
We prove the intermediate claim HUyOpenX: (U ∩ Y) ∈ Tx.
An exact proof term for the current goal is (lemma_intersection_two_open X Tx U Y HTx HUinTx HYinTx).
We prove the intermediate claim HUyOpenY: (U ∩ Y) ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_topologyI X Tx Y U HUinTx).
We prove the intermediate claim HclYeq: closure_of Y (subspace_topology X Tx Y) A = A.
An exact proof term for the current goal is (closed_closure_eq Y (subspace_topology X Tx Y) A HTy HclosedY).
We prove the intermediate claim HclSub: closure_of Y (subspace_topology X Tx Y) A = (closure_of X Tx A) ∩ Y.
An exact proof term for the current goal is (closure_in_subspace X Tx Y A HTx HYsub HAsubY).
We prove the intermediate claim HAeq: A = (closure_of X Tx A) ∩ Y.
rewrite the current goal using HclYeq (from right to left) at position 1.
An exact proof term for the current goal is HclSub.
We prove the intermediate claim HUySubA: (U ∩ Y) ⊆ A.
Let z be given.
Assume Hz: z ∈ U ∩ Y.
We will prove z ∈ A.
rewrite the current goal using HAeq (from left to right).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (HUsub z (binintersectE1 U Y z Hz)).
An exact proof term for the current goal is (binintersectE2 U Y z Hz).
We prove the intermediate claim HyIntY: y ∈ interior_of Y (subspace_topology X Tx Y) A.
We prove the intermediate claim HdefInt: interior_of Y (subspace_topology X Tx Y) A = {y0 ∈ Y|∃W : set, W ∈ subspace_topology X Tx Y ∧ y0 ∈ W ∧ W ⊆ A}.
Use reflexivity.
rewrite the current goal using HdefInt (from left to right).
Apply (SepI Y (λy0 : set ⇒ ∃W : set, W ∈ subspace_topology X Tx Y ∧ y0 ∈ W ∧ W ⊆ A) y) to the current goal.
An exact proof term for the current goal is HyY.
We use (U ∩ Y) to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is HUyOpenY.
An exact proof term for the current goal is (binintersectI U Y y HyU HyY).
An exact proof term for the current goal is HUySubA.
We prove the intermediate claim HyEmpty: y ∈ Empty.
rewrite the current goal using HintY (from right to left).
An exact proof term for the current goal is HyIntY.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE y HyEmpty).
Let x be given.
Assume HxE: x ∈ Empty.
We will prove x ∈ interior_of X Tx (closure_of X Tx A).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
Apply andI to the current goal.
We will prove closed_in X Tx C.
rewrite the current goal using HeqC (from left to right).
An exact proof term for the current goal is HclosedX.
We will prove interior_of X Tx C = Empty.
rewrite the current goal using HeqC (from left to right).
An exact proof term for the current goal is HintX.
We prove the intermediate claim HintUnionX: interior_of X Tx (⋃ FamX) = Empty.
An exact proof term for the current goal is (HpropX FamX HcountX HFamX).
We prove the intermediate claim HUnionSub: ⋃ Fam ⊆ ⋃ FamX.
Let z be given.
Assume Hz: z ∈ ⋃ Fam.
We will prove z ∈ ⋃ FamX.
Apply (UnionE_impred Fam z Hz (z ∈ ⋃ FamX)) to the current goal.
Let A be given.
Assume HzA: z ∈ A.
Assume HAin: A ∈ Fam.
We prove the intermediate claim HAsubY: A ⊆ Y.
An exact proof term for the current goal is (closed_in_subset Y (subspace_topology X Tx Y) A (andEL (closed_in Y (subspace_topology X Tx Y) A) (interior_of Y (subspace_topology X Tx Y) A = Empty) (HFam A HAin))).
We prove the intermediate claim HAsubX: A ⊆ X.
Let a be given.
Assume HaA: a ∈ A.
An exact proof term for the current goal is (HYsub a (HAsubY a HaA)).
We prove the intermediate claim Hzcl: z ∈ closure_of X Tx A.
An exact proof term for the current goal is (subset_of_closure X Tx A HTx HAsubX z HzA).
We prove the intermediate claim Hmem: (closure_of X Tx A) ∈ FamX.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HAin).
An exact proof term for the current goal is (UnionI FamX z (closure_of X Tx A) Hzcl Hmem).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ interior_of Y (subspace_topology X Tx Y) (⋃ Fam).
We will prove y ∈ Empty.
We prove the intermediate claim HexW: ∃W : set, W ∈ subspace_topology X Tx Y ∧ y ∈ W ∧ W ⊆ ⋃ Fam.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ ∃W : set, W ∈ subspace_topology X Tx Y ∧ y0 ∈ W ∧ W ⊆ ⋃ Fam) y Hy).
Apply HexW to the current goal.
Let W be given.
Assume HW: W ∈ subspace_topology X Tx Y ∧ y ∈ W ∧ W ⊆ ⋃ Fam.
We prove the intermediate claim HW12: W ∈ subspace_topology X Tx Y ∧ y ∈ W.
An exact proof term for the current goal is (andEL (W ∈ subspace_topology X Tx Y ∧ y ∈ W) (W ⊆ ⋃ Fam) HW).
We prove the intermediate claim HWTy: W ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andEL (W ∈ subspace_topology X Tx Y) (y ∈ W) HW12).
We prove the intermediate claim HyW: y ∈ W.
An exact proof term for the current goal is (andER (W ∈ subspace_topology X Tx Y) (y ∈ W) HW12).
We prove the intermediate claim HWsubU: W ⊆ ⋃ Fam.
An exact proof term for the current goal is (andER (W ∈ subspace_topology X Tx Y ∧ y ∈ W) (W ⊆ ⋃ Fam) HW).
We prove the intermediate claim HexV: ∃V ∈ Tx, W = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y W HWTy).
Apply HexV to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ W = V ∩ Y.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (W = V ∩ Y) HV).
We prove the intermediate claim HWdef: W = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (W = V ∩ Y) HV).
We prove the intermediate claim HWTx: W ∈ Tx.
rewrite the current goal using HWdef (from left to right).
An exact proof term for the current goal is (lemma_intersection_two_open X Tx V Y HTx HVTx HYinTx).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λy0 : set ⇒ ∃W0 : set, W0 ∈ subspace_topology X Tx Y ∧ y0 ∈ W0 ∧ W0 ⊆ ⋃ Fam) y Hy).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsub y HyY).
We prove the intermediate claim HyW_X: y ∈ W.
An exact proof term for the current goal is HyW.
We prove the intermediate claim HWsubUnionX: W ⊆ ⋃ FamX.
Let z be given.
Assume HzW: z ∈ W.
We prove the intermediate claim HzUnion: z ∈ ⋃ Fam.
An exact proof term for the current goal is (HWsubU z HzW).
An exact proof term for the current goal is (HUnionSub z HzUnion).
We prove the intermediate claim HyIntX: y ∈ interior_of X Tx (⋃ FamX).
We prove the intermediate claim HdefIntX: interior_of X Tx (⋃ FamX) = {x0 ∈ X|∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ ⋃ FamX}.
Use reflexivity.
rewrite the current goal using HdefIntX (from left to right).
Apply (SepI X (λx0 : set ⇒ ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ ⋃ FamX) y HyX) to the current goal.
We use W to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is HWTx.
An exact proof term for the current goal is HyW_X.
An exact proof term for the current goal is HWsubUnionX.
We prove the intermediate claim HyEmpty: y ∈ Empty.
rewrite the current goal using HintUnionX (from right to left).
An exact proof term for the current goal is HyIntX.
An exact proof term for the current goal is HyEmpty.
Let y be given.
Assume HyE: y ∈ Empty.
We will prove y ∈ interior_of Y (subspace_topology X Tx Y) (⋃ Fam).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE y HyE).
An exact proof term for the current goal is (Baire_space_closed_imp Y (subspace_topology X Tx Y) HBcY).
∎