Let X and Tx be given.
We will prove completely_normal_space X Tx ↔ (one_point_sets_closed X Tx ∧ (∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty)).
Apply iffI to the current goal.
Assume Hcn: completely_normal_space X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y)) Hcn).
We prove the intermediate claim Hall: ∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (andER (topology_on X Tx) (∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y)) Hcn).
We will prove one_point_sets_closed X Tx ∧ ∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We prove the intermediate claim HnormXsub: normal_space X (subspace_topology X Tx X).
An exact proof term for the current goal is (Hall X (Subq_ref X)).
We prove the intermediate claim HnormX: normal_space X Tx.
We will prove normal_space X Tx.
rewrite the current goal using (subspace_topology_whole X Tx HTx) (from right to left).
An exact proof term for the current goal is HnormXsub.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) HnormX).
Let A and B be given.
Assume Hsep: separated_subsets X Tx A B.
We prove the intermediate claim H123: (A ⊆ X ∧ B ⊆ X) ∧ closure_of X Tx A ∩ B = Empty.
An exact proof term for the current goal is (andEL ((A ⊆ X ∧ B ⊆ X) ∧ closure_of X Tx A ∩ B = Empty) (A ∩ closure_of X Tx B = Empty) Hsep).
We prove the intermediate claim H4: A ∩ closure_of X Tx B = Empty.
An exact proof term for the current goal is (andER ((A ⊆ X ∧ B ⊆ X) ∧ closure_of X Tx A ∩ B = Empty) (A ∩ closure_of X Tx B = Empty) Hsep).
We prove the intermediate claim H12: A ⊆ X ∧ B ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X ∧ B ⊆ X) (closure_of X Tx A ∩ B = Empty) H123).
We prove the intermediate claim H3: closure_of X Tx A ∩ B = Empty.
An exact proof term for the current goal is (andER (A ⊆ X ∧ B ⊆ X) (closure_of X Tx A ∩ B = Empty) H123).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (B ⊆ X) H12).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (andER (A ⊆ X) (B ⊆ X) H12).
Set CA to be the term closure_of X Tx A of type set.
Set CB to be the term closure_of X Tx B of type set.
Set Y to be the term X ∖ (CA ∩ CB) of type set.
We prove the intermediate claim HYsubX: Y ⊆ X.
An exact proof term for the current goal is (setminus_Subq X (CA ∩ CB)).
We prove the intermediate claim HnormY: normal_space Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (Hall Y HYsubX).
We prove the intermediate claim HTy: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (normal_space_topology_on Y (subspace_topology X Tx Y) HnormY).
We prove the intermediate claim HAsubY: A ⊆ Y.
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HanotCB: a ∉ CB.
Assume HaCB: a ∈ CB.
We prove the intermediate claim HaACB: a ∈ A ∩ CB.
An exact proof term for the current goal is (binintersectI A CB a HaA HaCB).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is HaACB.
We will prove False.
An exact proof term for the current goal is (EmptyE a HaE).
We prove the intermediate claim HanotCap: a ∉ CA ∩ CB.
Assume HaCap: a ∈ CA ∩ CB.
We prove the intermediate claim HaCB: a ∈ CB.
An exact proof term for the current goal is (binintersectE2 CA CB a HaCap).
We will prove False.
An exact proof term for the current goal is (HanotCB HaCB).
An exact proof term for the current goal is (setminusI X (CA ∩ CB) a HaX HanotCap).
We prove the intermediate claim HBsubY: B ⊆ Y.
Let b be given.
Assume HbB: b ∈ B.
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim HbnotCA: b ∉ CA.
Assume HbCA: b ∈ CA.
We prove the intermediate claim HbCAB: b ∈ CA ∩ B.
An exact proof term for the current goal is (binintersectI CA B b HbCA HbB).
We prove the intermediate claim HbE: b ∈ Empty.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is HbCAB.
We will prove False.
An exact proof term for the current goal is (EmptyE b HbE).
We prove the intermediate claim HbnotCap: b ∉ CA ∩ CB.
Assume HbCap: b ∈ CA ∩ CB.
We prove the intermediate claim HbCA: b ∈ CA.
An exact proof term for the current goal is (binintersectE1 CA CB b HbCap).
We will prove False.
An exact proof term for the current goal is (HbnotCA HbCA).
An exact proof term for the current goal is (setminusI X (CA ∩ CB) b HbX HbnotCap).
Set clA to be the term closure_of Y (subspace_topology X Tx Y) A of type set.
Set clB to be the term closure_of Y (subspace_topology X Tx Y) B of type set.
We prove the intermediate claim HclAeq: clA = CA ∩ Y.
An exact proof term for the current goal is (closure_in_subspace X Tx Y A HTx HYsubX HAsubY).
We prove the intermediate claim HclBeq: clB = CB ∩ Y.
An exact proof term for the current goal is (closure_in_subspace X Tx Y B HTx HYsubX HBsubY).
We prove the intermediate claim HclAclosed: closed_in Y (subspace_topology X Tx Y) clA.
An exact proof term for the current goal is (closure_is_closed Y (subspace_topology X Tx Y) A HTy HAsubY).
We prove the intermediate claim HclBclosed: closed_in Y (subspace_topology X Tx Y) clB.
An exact proof term for the current goal is (closure_is_closed Y (subspace_topology X Tx Y) B HTy HBsubY).
We prove the intermediate claim HclAclBEmpty: clA ∩ clB = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx: x ∈ clA ∩ clB.
We prove the intermediate claim HxclA: x ∈ clA.
An exact proof term for the current goal is (binintersectE1 clA clB x Hx).
We prove the intermediate claim HxclB: x ∈ clB.
An exact proof term for the current goal is (binintersectE2 clA clB x Hx).
We prove the intermediate claim HxY: x ∈ Y.
We prove the intermediate claim HxCAcapY: x ∈ CA ∩ Y.
rewrite the current goal using HclAeq (from right to left).
An exact proof term for the current goal is HxclA.
An exact proof term for the current goal is (binintersectE2 CA Y x HxCAcapY).
We prove the intermediate claim HxnotCap: x ∉ CA ∩ CB.
An exact proof term for the current goal is (setminusE2 X (CA ∩ CB) x HxY).
We prove the intermediate claim HxCA: x ∈ CA.
We prove the intermediate claim HxCAcapY: x ∈ CA ∩ Y.
rewrite the current goal using HclAeq (from right to left).
An exact proof term for the current goal is HxclA.
An exact proof term for the current goal is (binintersectE1 CA Y x HxCAcapY).
We prove the intermediate claim HxCB: x ∈ CB.
We prove the intermediate claim HxCBcapY: x ∈ CB ∩ Y.
rewrite the current goal using HclBeq (from right to left).
An exact proof term for the current goal is HxclB.
An exact proof term for the current goal is (binintersectE1 CB Y x HxCBcapY).
We prove the intermediate claim HxCap: x ∈ CA ∩ CB.
An exact proof term for the current goal is (binintersectI CA CB x HxCA HxCB).
We will prove x ∈ Empty.
We will prove False.
An exact proof term for the current goal is (HxnotCap HxCap).
We prove the intermediate claim HsepY: ∀P Q : set, closed_in Y (subspace_topology X Tx Y) P → closed_in Y (subspace_topology X Tx Y) Q → P ∩ Q = Empty → ∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ P ⊆ U ∧ Q ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed Y (subspace_topology X Tx Y)) (∀P Q : set, closed_in Y (subspace_topology X Tx Y) P → closed_in Y (subspace_topology X Tx Y) Q → P ∩ Q = Empty → ∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ P ⊆ U ∧ Q ⊆ V ∧ U ∩ V = Empty) HnormY).
We prove the intermediate claim HexUVY: ∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ clA ⊆ U ∧ clB ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HsepY clA clB HclAclosed HclBclosed HclAclBEmpty).
Apply HexUVY to the current goal.
Let U' be given.
Assume HU': ∃V' : set, U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y ∧ clA ⊆ U' ∧ clB ⊆ V' ∧ U' ∩ V' = Empty.
Apply HU' to the current goal.
Let V' be given.
Assume HUV': U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y ∧ clA ⊆ U' ∧ clB ⊆ V' ∧ U' ∩ V' = Empty.
We prove the intermediate claim H1234: ((U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) ∧ clA ⊆ U') ∧ clB ⊆ V'.
An exact proof term for the current goal is (andEL (((U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) ∧ clA ⊆ U') ∧ clB ⊆ V') (U' ∩ V' = Empty) HUV').
We prove the intermediate claim HUVEmpty: U' ∩ V' = Empty.
An exact proof term for the current goal is (andER (((U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) ∧ clA ⊆ U') ∧ clB ⊆ V') (U' ∩ V' = Empty) HUV').
We prove the intermediate claim H123: (U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) ∧ clA ⊆ U'.
An exact proof term for the current goal is (andEL ((U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) ∧ clA ⊆ U') (clB ⊆ V') H1234).
We prove the intermediate claim H4V: clB ⊆ V'.
An exact proof term for the current goal is (andER ((U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) ∧ clA ⊆ U') (clB ⊆ V') H1234).
We prove the intermediate claim H12: U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andEL (U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) (clA ⊆ U') H123).
We prove the intermediate claim H3U: clA ⊆ U'.
An exact proof term for the current goal is (andER (U' ∈ subspace_topology X Tx Y ∧ V' ∈ subspace_topology X Tx Y) (clA ⊆ U') H123).
We prove the intermediate claim HU'in: U' ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andEL (U' ∈ subspace_topology X Tx Y) (V' ∈ subspace_topology X Tx Y) H12).
We prove the intermediate claim HV'in: V' ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andER (U' ∈ subspace_topology X Tx Y) (V' ∈ subspace_topology X Tx Y) H12).
We prove the intermediate claim HopU': open_in Y (subspace_topology X Tx Y) U'.
An exact proof term for the current goal is (open_inI Y (subspace_topology X Tx Y) U' HTy HU'in).
We prove the intermediate claim HopV': open_in Y (subspace_topology X Tx Y) V'.
An exact proof term for the current goal is (open_inI Y (subspace_topology X Tx Y) V' HTy HV'in).
We prove the intermediate claim HU'subY: U' ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y (subspace_topology X Tx Y) U' HTy HU'in).
We prove the intermediate claim HV'subY: V' ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y (subspace_topology X Tx Y) V' HTy HV'in).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, U' = U0 ∩ Y.
An exact proof term for the current goal is (iffEL (open_in Y (subspace_topology X Tx Y) U') (∃U0 ∈ Tx, U' = U0 ∩ Y) (open_in_subspace_iff X Tx Y U' HTx HYsubX HU'subY) HopU').
We prove the intermediate claim HexV0: ∃V0 ∈ Tx, V' = V0 ∩ Y.
An exact proof term for the current goal is (iffEL (open_in Y (subspace_topology X Tx Y) V') (∃V0 ∈ Tx, V' = V0 ∩ Y) (open_in_subspace_iff X Tx Y V' HTx HYsubX HV'subY) HopV').
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pair: U0 ∈ Tx ∧ U' = U0 ∩ Y.
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pair: V0 ∈ Tx ∧ V' = V0 ∩ Y.
We prove the intermediate claim HU0: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (U' = U0 ∩ Y) HU0pair).
We prove the intermediate claim HU'eq: U' = U0 ∩ Y.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (U' = U0 ∩ Y) HU0pair).
We prove the intermediate claim HV0: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (V' = V0 ∩ Y) HV0pair).
We prove the intermediate claim HV'eq: V' = V0 ∩ Y.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (V' = V0 ∩ Y) HV0pair).
We prove the intermediate claim HUV0subCap: U0 ∩ V0 ⊆ CA ∩ CB.
Let x be given.
Assume HxUV: x ∈ U0 ∩ V0.
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 V0 x HxUV).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (binintersectE2 U0 V0 x HxUV).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0 x HxU0).
Apply (xm (x ∈ CA ∩ CB)) to the current goal.
Assume HxCap: x ∈ CA ∩ CB.
An exact proof term for the current goal is HxCap.
Assume HxnotCap: ¬ (x ∈ CA ∩ CB).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (setminusI X (CA ∩ CB) x HxX HxnotCap).
We prove the intermediate claim HxU': x ∈ U'.
rewrite the current goal using HU'eq (from left to right).
An exact proof term for the current goal is (binintersectI U0 Y x HxU0 HxY).
We prove the intermediate claim HxV': x ∈ V'.
rewrite the current goal using HV'eq (from left to right).
An exact proof term for the current goal is (binintersectI V0 Y x HxV0 HxY).
We prove the intermediate claim HxUV': x ∈ U' ∩ V'.
An exact proof term for the current goal is (binintersectI U' V' x HxU' HxV').
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVEmpty (from right to left).
An exact proof term for the current goal is HxUV'.
We will prove x ∈ CA ∩ CB.
We will prove False.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim HCAclosed: closed_in X Tx CA.
An exact proof term for the current goal is (closure_is_closed X Tx A HTx HAsubX).
We prove the intermediate claim HCBclosed: closed_in X Tx CB.
An exact proof term for the current goal is (closure_is_closed X Tx B HTx HBsubX).
We prove the intermediate claim HopCAc: open_in X Tx (X ∖ CA).
An exact proof term for the current goal is (open_of_closed_complement X Tx CA HCAclosed).
We prove the intermediate claim HopCBc: open_in X Tx (X ∖ CB).
An exact proof term for the current goal is (open_of_closed_complement X Tx CB HCBclosed).
We prove the intermediate claim HCAc_in: X ∖ CA ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ CA) HopCAc).
We prove the intermediate claim HCBc_in: X ∖ CB ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ CB) HopCBc).
Set U to be the term U0 ∩ (X ∖ CB) of type set.
Set V to be the term V0 ∩ (X ∖ CA) of type set.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx U0 HU0 (X ∖ CB) HCBc_in).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx V0 HV0 (X ∖ CA) HCAc_in).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We will prove open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove (open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V).
Apply andI to the current goal.
We will prove (open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U).
Apply andI to the current goal.
We will prove open_in X Tx U ∧ open_in X Tx V.
Apply andI to the current goal.
An exact proof term for the current goal is (open_inI X Tx U HTx HUinTx).
An exact proof term for the current goal is (open_inI X Tx V HTx HVinTx).
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaU': a ∈ U'.
We prove the intermediate claim HAclA: A ⊆ clA.
An exact proof term for the current goal is (subset_of_closure Y (subspace_topology X Tx Y) A HTy HAsubY).
We prove the intermediate claim Ha_clA: a ∈ clA.
An exact proof term for the current goal is (HAclA a HaA).
An exact proof term for the current goal is (H3U a Ha_clA).
We prove the intermediate claim HaU0: a ∈ U0.
We prove the intermediate claim HaU0capY: a ∈ U0 ∩ Y.
rewrite the current goal using HU'eq (from right to left).
An exact proof term for the current goal is HaU'.
An exact proof term for the current goal is (binintersectE1 U0 Y a HaU0capY).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HanotCB: a ∉ CB.
Assume HaCB: a ∈ CB.
We prove the intermediate claim HaACB: a ∈ A ∩ CB.
An exact proof term for the current goal is (binintersectI A CB a HaA HaCB).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is HaACB.
We will prove False.
An exact proof term for the current goal is (EmptyE a HaE).
We prove the intermediate claim HaXminusCB: a ∈ X ∖ CB.
An exact proof term for the current goal is (setminusI X CB a HaX HanotCB).
An exact proof term for the current goal is (binintersectI U0 (X ∖ CB) a HaU0 HaXminusCB).
Let b be given.
Assume HbB: b ∈ B.
We prove the intermediate claim HbV': b ∈ V'.
We prove the intermediate claim HBclB: B ⊆ clB.
An exact proof term for the current goal is (subset_of_closure Y (subspace_topology X Tx Y) B HTy HBsubY).
We prove the intermediate claim Hb_clB: b ∈ clB.
An exact proof term for the current goal is (HBclB b HbB).
An exact proof term for the current goal is (H4V b Hb_clB).
We prove the intermediate claim HbV0: b ∈ V0.
We prove the intermediate claim HbV0capY: b ∈ V0 ∩ Y.
rewrite the current goal using HV'eq (from right to left).
An exact proof term for the current goal is HbV'.
An exact proof term for the current goal is (binintersectE1 V0 Y b HbV0capY).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
We prove the intermediate claim HbnotCA: b ∉ CA.
Assume HbCA: b ∈ CA.
We prove the intermediate claim HbCAB: b ∈ CA ∩ B.
An exact proof term for the current goal is (binintersectI CA B b HbCA HbB).
We prove the intermediate claim HbE: b ∈ Empty.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is HbCAB.
We will prove False.
An exact proof term for the current goal is (EmptyE b HbE).
We prove the intermediate claim HbXminusCA: b ∈ X ∖ CA.
An exact proof term for the current goal is (setminusI X CA b HbX HbnotCA).
We prove the intermediate claim HbV: b ∈ V.
An exact proof term for the current goal is (binintersectI V0 (X ∖ CA) b HbV0 HbXminusCA).
An exact proof term for the current goal is HbV.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxUV: x ∈ U ∩ V.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x HxUV).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x HxUV).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 (X ∖ CB) x HxU).
We prove the intermediate claim HxNotCB: x ∉ CB.
An exact proof term for the current goal is (setminusE2 X CB x (binintersectE2 U0 (X ∖ CB) x HxU)).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (binintersectE1 V0 (X ∖ CA) x HxV).
We prove the intermediate claim HxCap0: x ∈ U0 ∩ V0.
An exact proof term for the current goal is (binintersectI U0 V0 x HxU0 HxV0).
We prove the intermediate claim HxCap: x ∈ CA ∩ CB.
An exact proof term for the current goal is (HUV0subCap x HxCap0).
We prove the intermediate claim HxCB: x ∈ CB.
An exact proof term for the current goal is (binintersectE2 CA CB x HxCap).
We will prove x ∈ Empty.
We will prove False.
An exact proof term for the current goal is (HxNotCB HxCB).
Assume Hrhs: one_point_sets_closed X Tx ∧ (∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HoneX: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hrhs).
We prove the intermediate claim Hsep2: ∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A B : set, separated_subsets X Tx A B → ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hrhs).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HoneX).
We prove the intermediate claim HallCN: ∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y).
Let Y be given.
Assume HYsubX: Y ⊆ X.
We will prove normal_space Y (subspace_topology X Tx Y).
Set Ty to be the term subspace_topology X Tx Y.
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 HoneY: one_point_sets_closed Y Ty.
We will prove topology_on Y Ty ∧ ∀y : set, y ∈ Y → closed_in Y Ty {y}.
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 HsingX: ∀x : set, x ∈ X → closed_in X Tx {x}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HoneX).
We prove the intermediate claim HsingClosedX: closed_in X Tx {y}.
An exact proof term for the current goal is (HsingX y HyX).
Apply (iffER (closed_in Y Ty {y}) (∃C0 : set, closed_in X Tx C0 ∧ {y} = C0 ∩ Y) (closed_in_subspace_iff_intersection X Tx Y {y} HTx HYsubX)) to the current goal.
We use {y} to witness the existential quantifier.
We will prove closed_in X Tx {y} ∧ {y} = {y} ∩ Y.
Apply andI to the current goal.
An exact proof term for the current goal is HsingClosedX.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ {y}.
We will prove z ∈ {y} ∩ Y.
We prove the intermediate claim Hzy: z = y.
An exact proof term for the current goal is (SingE y z Hz).
We prove the intermediate claim HzY: z ∈ Y.
rewrite the current goal using Hzy (from left to right).
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (binintersectI {y} Y z Hz HzY).
Let z be given.
Assume Hz: z ∈ {y} ∩ Y.
We will prove z ∈ {y}.
An exact proof term for the current goal is (binintersectE1 {y} Y z Hz).
We prove the intermediate claim HnormSep: ∀C D : set, closed_in Y Ty C → closed_in Y Ty D → C ∩ D = Empty → ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty.
Let C and D be given.
Assume HCcl: closed_in Y Ty C.
Assume HDcl: closed_in Y Ty D.
Assume HCDemp: C ∩ D = Empty.
We prove the intermediate claim HCsubY: C ⊆ Y.
An exact proof term for the current goal is (closed_in_subset Y Ty C HCcl).
We prove the intermediate claim HDsubY: D ⊆ Y.
An exact proof term for the current goal is (closed_in_subset Y Ty D HDcl).
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (Subq_tra C Y X HCsubY HYsubX).
We prove the intermediate claim HDsubX: D ⊆ X.
An exact proof term for the current goal is (Subq_tra D Y X HDsubY HYsubX).
We prove the intermediate claim HsepCD: separated_subsets X Tx C D.
We will prove C ⊆ X ∧ D ⊆ X ∧ closure_of X Tx C ∩ D = Empty ∧ C ∩ closure_of X Tx D = Empty.
Apply andI to the current goal.
We will prove (C ⊆ X ∧ D ⊆ X ∧ closure_of X Tx C ∩ D = Empty).
Apply andI to the current goal.
We will prove C ⊆ X ∧ D ⊆ X.
Apply andI to the current goal.
An exact proof term for the current goal is HCsubX.
An exact proof term for the current goal is HDsubX.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx C ∩ D.
We prove the intermediate claim HxclC: x ∈ closure_of X Tx C.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx C) D x Hx).
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx C) D x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (HDsubY x HxD).
We prove the intermediate claim HxclCY: x ∈ closure_of X Tx C ∩ Y.
An exact proof term for the current goal is (binintersectI (closure_of X Tx C) Y x HxclC HxY).
We prove the intermediate claim HclCEq: closure_of Y Ty C = closure_of X Tx C ∩ Y.
An exact proof term for the current goal is (closure_in_subspace X Tx Y C HTx HYsubX HCsubY).
We prove the intermediate claim HxclY: x ∈ closure_of Y Ty C.
rewrite the current goal using HclCEq (from left to right).
An exact proof term for the current goal is HxclCY.
We prove the intermediate claim HclYeq: closure_of Y Ty C = C.
An exact proof term for the current goal is (closed_closure_eq Y Ty C HTy HCcl).
We prove the intermediate claim HxC: x ∈ C.
rewrite the current goal using HclYeq (from right to left).
An exact proof term for the current goal is HxclY.
We prove the intermediate claim HxCD: x ∈ C ∩ D.
An exact proof term for the current goal is (binintersectI C D x HxC HxD).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HCDemp (from right to left).
An exact proof term for the current goal is HxCD.
We will prove x ∈ Empty.
An exact proof term for the current goal is HxE.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx: x ∈ C ∩ closure_of X Tx D.
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (binintersectE1 C (closure_of X Tx D) x Hx).
We prove the intermediate claim HxclD: x ∈ closure_of X Tx D.
An exact proof term for the current goal is (binintersectE2 C (closure_of X Tx D) x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (HCsubY x HxC).
We prove the intermediate claim HxclDY: x ∈ closure_of X Tx D ∩ Y.
An exact proof term for the current goal is (binintersectI (closure_of X Tx D) Y x HxclD HxY).
We prove the intermediate claim HclDEq: closure_of Y Ty D = closure_of X Tx D ∩ Y.
An exact proof term for the current goal is (closure_in_subspace X Tx Y D HTx HYsubX HDsubY).
We prove the intermediate claim HxclY: x ∈ closure_of Y Ty D.
rewrite the current goal using HclDEq (from left to right).
An exact proof term for the current goal is HxclDY.
We prove the intermediate claim HclYeq: closure_of Y Ty D = D.
An exact proof term for the current goal is (closed_closure_eq Y Ty D HTy HDcl).
We prove the intermediate claim HxD: x ∈ D.
rewrite the current goal using HclYeq (from right to left).
An exact proof term for the current goal is HxclY.
We prove the intermediate claim HxCD: x ∈ C ∩ D.
An exact proof term for the current goal is (binintersectI C D x HxC HxD).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HCDemp (from right to left).
An exact proof term for the current goal is HxCD.
We will prove x ∈ Empty.
An exact proof term for the current goal is HxE.
We prove the intermediate claim HexUVX: ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hsep2 C D HsepCD).
Apply HexUVX to the current goal.
Let U be given.
Assume HU: ∃V : set, open_in X Tx U ∧ open_in X Tx V ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty.
Apply HU to the current goal.
Let V be given.
Assume HUV: open_in X Tx U ∧ open_in X Tx V ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim H1234: (((open_in X Tx U ∧ open_in X Tx V) ∧ C ⊆ U) ∧ D ⊆ V).
An exact proof term for the current goal is (andEL ((((open_in X Tx U ∧ open_in X Tx V) ∧ C ⊆ U) ∧ D ⊆ V)) (U ∩ V = Empty) HUV).
We prove the intermediate claim HUVEmpty: U ∩ V = Empty.
An exact proof term for the current goal is (andER ((((open_in X Tx U ∧ open_in X Tx V) ∧ C ⊆ U) ∧ D ⊆ V)) (U ∩ V = Empty) HUV).
We prove the intermediate claim H123: (open_in X Tx U ∧ open_in X Tx V) ∧ C ⊆ U.
An exact proof term for the current goal is (andEL ((open_in X Tx U ∧ open_in X Tx V) ∧ C ⊆ U) (D ⊆ V) H1234).
We prove the intermediate claim HDsubV: D ⊆ V.
An exact proof term for the current goal is (andER ((open_in X Tx U ∧ open_in X Tx V) ∧ C ⊆ U) (D ⊆ V) H1234).
We prove the intermediate claim H12: open_in X Tx U ∧ open_in X Tx V.
An exact proof term for the current goal is (andEL (open_in X Tx U ∧ open_in X Tx V) (C ⊆ U) H123).
We prove the intermediate claim HCsubU: C ⊆ U.
An exact proof term for the current goal is (andER (open_in X Tx U ∧ open_in X Tx V) (C ⊆ U) H123).
We prove the intermediate claim HopenU: open_in X Tx U.
An exact proof term for the current goal is (andEL (open_in X Tx U) (open_in X Tx V) H12).
We prove the intermediate claim HopenV: open_in X Tx V.
An exact proof term for the current goal is (andER (open_in X Tx U) (open_in X Tx V) H12).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HopenU).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx V HopenV).
Set UY to be the term U ∩ Y.
Set VY to be the term V ∩ Y.
We use UY to witness the existential quantifier.
We use VY to witness the existential quantifier.
We will prove UY ∈ Ty ∧ VY ∈ Ty ∧ C ⊆ UY ∧ D ⊆ VY ∧ UY ∩ VY = Empty.
Apply andI to the current goal.
We will prove (UY ∈ Ty ∧ VY ∈ Ty ∧ C ⊆ UY ∧ D ⊆ VY).
Apply andI to the current goal.
We will prove (UY ∈ Ty ∧ VY ∈ Ty ∧ C ⊆ UY).
Apply andI to the current goal.
We will prove UY ∈ Ty ∧ VY ∈ Ty.
Apply andI to the current goal.
An exact proof term for the current goal is (subspace_topologyI X Tx Y U HUinTx).
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HVinTx).
Let x be given.
Assume HxC: x ∈ C.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (HCsubU x HxC).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (HCsubY x HxC).
An exact proof term for the current goal is (binintersectI U Y x HxU HxY).
Let x be given.
Assume HxD: x ∈ D.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HDsubV x HxD).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (HDsubY x HxD).
An exact proof term for the current goal is (binintersectI V Y x HxV HxY).
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxCap: x ∈ UY ∩ VY.
We prove the intermediate claim HxUY: x ∈ UY.
An exact proof term for the current goal is (binintersectE1 UY VY x HxCap).
We prove the intermediate claim HxVY: x ∈ VY.
An exact proof term for the current goal is (binintersectE2 UY VY x HxCap).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U Y x HxUY).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVEmpty (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is HxE.
An exact proof term for the current goal is (andI (one_point_sets_closed Y Ty) (∀C D : set, closed_in Y Ty C → closed_in Y Ty D → C ∩ D = Empty → ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ C ⊆ U ∧ D ⊆ V ∧ U ∩ V = Empty) HoneY HnormSep).
An exact proof term for the current goal is (andI (topology_on X Tx) (∀Y : set, Y ⊆ X → normal_space Y (subspace_topology X Tx Y)) HTx HallCN).
∎