We will prove regular_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology ∧ ¬ normal_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.
Apply andI to the current goal.
We prove the intermediate claim HdefTop: Sorgenfrey_plane_topology = product_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology.
Use reflexivity.
rewrite the current goal using HdefTop (from left to right).
An exact proof term for the current goal is (product_topology_regular Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line_regular Sorgenfrey_line_regular).
Assume Hnorm: normal_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.
We will prove False.
Set X to be the term setprod Sorgenfrey_line Sorgenfrey_line.
Set Tx to be the term Sorgenfrey_plane_topology.
Set L to be the term Sorgenfrey_plane_L.
Set D to be the term Sorgenfrey_plane_rational_points.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HcountD: countable_set D.
An exact proof term for the current goal is Sorgenfrey_plane_rational_points_countable.
We prove the intermediate claim Hdense: closure_of X Tx D = X.
An exact proof term for the current goal is Sorgenfrey_plane_rational_points_dense.
We prove the intermediate claim HLcl: closed_in X Tx L.
An exact proof term for the current goal is Sorgenfrey_plane_L_closed.
We prove the intermediate claim HLsubX: L ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx L HLcl).
Set Ta to be the term subspace_topology X Tx L.
We prove the intermediate claim HTa: topology_on L Ta.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx L HTx HLsubX).
We prove the intermediate claim HTaEq: Ta = discrete_topology L.
We prove the intermediate claim HdefTa: Ta = subspace_topology X Tx L.
Use reflexivity.
rewrite the current goal using HdefTa (from left to right).
An exact proof term for the current goal is Sorgenfrey_plane_L_subspace_discrete.
We prove the intermediate claim HsepFn: ∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀A0 B0 : set, closed_in X Tx A0 → closed_in X Tx B0 → A0 ∩ B0 = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A0 ⊆ U ∧ B0 ⊆ V ∧ U ∩ V = Empty) Hnorm).
Set UV to be the term λA : set ⇒ Eps_i (λW : set ⇒ ∃U V : set, W = (U,V) ∧ (U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty)).
Set Uof to be the term λA : set ⇒ (UV A) 0.
Set Vof to be the term λA : set ⇒ (UV A) 1.
Set theta to be the term λA : set ⇒ D ∩ (Uof A).
We prove the intermediate claim HUV_ok: ∀A ∈ 𝒫 L, ∃U V : set, UV A = (U,V) ∧ (U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty).
Let A be given.
Assume HA: A ∈ 𝒫 L.
We will prove ∃U V : set, UV A = (U,V) ∧ (U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HAsubL: A ⊆ L.
An exact proof term for the current goal is (PowerE L A HA).
We prove the intermediate claim HAcSubL: (L ∖ A) ⊆ L.
Apply setminus_Subq to the current goal.
We prove the intermediate claim HAopenTa: A ∈ Ta.
rewrite the current goal using HTaEq (from left to right).
An exact proof term for the current goal is (PowerI L A HAsubL).
We prove the intermediate claim HAcopenTa: (L ∖ A) ∈ Ta.
rewrite the current goal using HTaEq (from left to right).
An exact proof term for the current goal is (PowerI L (L ∖ A) HAcSubL).
We prove the intermediate claim HAcclTa0: closed_in L Ta (L ∖ (L ∖ A)).
An exact proof term for the current goal is (closed_of_open_complement L Ta (L ∖ A) HTa HAcopenTa).
We prove the intermediate claim Hsetminus1: L ∖ (L ∖ A) = A.
An exact proof term for the current goal is (setminus_setminus_eq L A HAsubL).
We prove the intermediate claim HAclTa: closed_in L Ta A.
rewrite the current goal using Hsetminus1 (from right to left).
An exact proof term for the current goal is HAcclTa0.
We prove the intermediate claim HAcclTa: closed_in L Ta (L ∖ A).
An exact proof term for the current goal is (closed_of_open_complement L Ta A HTa HAopenTa).
We prove the intermediate claim HAcl: closed_in X Tx A.
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx L A HLcl HAclTa).
We prove the intermediate claim HAccl: closed_in X Tx (L ∖ A).
An exact proof term for the current goal is (ex17_2_closed_in_closed_subspace X Tx L (L ∖ A) HLcl HAcclTa).
We prove the intermediate claim Hdisj: A ∩ (L ∖ A) = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ A ∩ (L ∖ A).
We will prove x ∈ Empty.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A (L ∖ A) x Hx).
We prove the intermediate claim HxAc: x ∈ (L ∖ A).
An exact proof term for the current goal is (binintersectE2 A (L ∖ A) x Hx).
We prove the intermediate claim HxNotA: x ∉ A.
An exact proof term for the current goal is (andER (x ∈ L) (x ∉ A) (setminusE L A x HxAc)).
An exact proof term for the current goal is (FalseE (HxNotA HxA) (x ∈ Empty)).
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ A ∩ (L ∖ A).
An exact proof term for the current goal is (EmptyE x Hx (x ∈ A ∩ (L ∖ A))).
We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HsepFn A (L ∖ A) HAcl HAccl Hdisj).
We prove the intermediate claim HexW: ∃W : set, (∃U V : set, W = (U,V) ∧ (U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty)).
Apply HexUV to the current goal.
Let U be given.
Assume HexV.
Apply HexV to the current goal.
Let V be given.
Assume HUV.
We use (U,V) to witness the existential quantifier.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is HUV.
We prove the intermediate claim HUVeps: ∃U V : set, UV A = (U,V) ∧ (U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty).
An exact proof term for the current goal is (Eps_i_ex (λW : set ⇒ ∃U V : set, W = (U,V) ∧ (U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ (L ∖ A) ⊆ V ∧ U ∩ V = Empty)) HexW).
An exact proof term for the current goal is HUVeps.
We prove the intermediate claim Htheta_inj: inj (𝒫 L) (𝒫 D) theta.
Apply (injI (𝒫 L) (𝒫 D) theta) to the current goal.
Let A be given.
Assume HA: A ∈ 𝒫 L.
We will prove theta A ∈ 𝒫 D.
Apply PowerI to the current goal.
An exact proof term for the current goal is (binintersect_Subq_1 D (Uof A)).
Let A be given.
Assume HA: A ∈ 𝒫 L.
Let B be given.
Assume HB: B ∈ 𝒫 L.
Assume Heq: theta A = theta B.
We will prove A = B.
We prove the intermediate claim HAB: A ⊆ B.
Let p be given.
Assume HpA: p ∈ A.
We will prove p ∈ B.
Apply xm (p ∈ B) to the current goal.
Assume HpB: p ∈ B.
An exact proof term for the current goal is HpB.
Assume HpNotB: p ∉ B.
We will prove p ∈ B.
We prove the intermediate claim HAsubL: A ⊆ L.
An exact proof term for the current goal is (PowerE L A HA).
We prove the intermediate claim HBsubL: B ⊆ L.
An exact proof term for the current goal is (PowerE L B HB).
We prove the intermediate claim HpL: p ∈ L.
An exact proof term for the current goal is (HAsubL p HpA).
We prove the intermediate claim HpLB: p ∈ (L ∖ B).
An exact proof term for the current goal is (setminusI L B p HpL HpNotB).
We prove the intermediate claim HexA: ∃U1 V1 : set, UV A = (U1,V1) ∧ (U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty).
An exact proof term for the current goal is (HUV_ok A HA).
We prove the intermediate claim HexB: ∃U2 V2 : set, UV B = (U2,V2) ∧ (U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty).
An exact proof term for the current goal is (HUV_ok B HB).
Apply HexA to the current goal.
Let U1 be given.
Assume HexV1.
Apply HexV1 to the current goal.
Let V1 be given.
Assume HpackA.
Apply HexB to the current goal.
Let U2 be given.
Assume HexV2.
Apply HexV2 to the current goal.
Let V2 be given.
Assume HpackB.
We prove the intermediate claim HUV_A: UV A = (U1,V1).
An exact proof term for the current goal is (andEL (UV A = (U1,V1)) (U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty) HpackA).
We prove the intermediate claim HUV_B: UV B = (U2,V2).
An exact proof term for the current goal is (andEL (UV B = (U2,V2)) (U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty) HpackB).
We prove the intermediate claim HpropsA: U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (andER (UV A = (U1,V1)) (U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty) HpackA).
We prove the intermediate claim HpropsB: U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty.
An exact proof term for the current goal is (andER (UV B = (U2,V2)) (U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty) HpackB).
We prove the intermediate claim HleftA: ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ∧ (L ∖ A) ⊆ V1.
An exact proof term for the current goal is (andEL (((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ∧ (L ∖ A) ⊆ V1) (U1 ∩ V1 = Empty) HpropsA).
We prove the intermediate claim HUV1pair: (U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1.
An exact proof term for the current goal is (andEL ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ((L ∖ A) ⊆ V1) HleftA).
We prove the intermediate claim HU1V1: U1 ∈ Tx ∧ V1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ V1 ∈ Tx) (A ⊆ U1) HUV1pair).
We prove the intermediate claim HU1: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (V1 ∈ Tx) HU1V1).
We prove the intermediate claim HAsubU1: A ⊆ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ V1 ∈ Tx) (A ⊆ U1) HUV1pair).
We prove the intermediate claim HleftB: ((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ∧ (L ∖ B) ⊆ V2.
An exact proof term for the current goal is (andEL (((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ∧ (L ∖ B) ⊆ V2) (U2 ∩ V2 = Empty) HpropsB).
We prove the intermediate claim HUV2pair: (U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2.
An exact proof term for the current goal is (andEL ((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ((L ∖ B) ⊆ V2) HleftB).
We prove the intermediate claim HU2V2: U2 ∈ Tx ∧ V2 ∈ Tx.
An exact proof term for the current goal is (andEL (U2 ∈ Tx ∧ V2 ∈ Tx) (B ⊆ U2) HUV2pair).
We prove the intermediate claim HV2: V2 ∈ Tx.
An exact proof term for the current goal is (andER (U2 ∈ Tx) (V2 ∈ Tx) HU2V2).
We prove the intermediate claim HLBsubV2: (L ∖ B) ⊆ V2.
An exact proof term for the current goal is (andER ((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ((L ∖ B) ⊆ V2) HleftB).
We prove the intermediate claim HdisjB: U2 ∩ V2 = Empty.
An exact proof term for the current goal is (andER (((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ∧ (L ∖ B) ⊆ V2) (U2 ∩ V2 = Empty) HpropsB).
We prove the intermediate claim HpU1: p ∈ U1.
An exact proof term for the current goal is (HAsubU1 p HpA).
We prove the intermediate claim HpV2: p ∈ V2.
An exact proof term for the current goal is (HLBsubV2 p HpLB).
Set W to be the term U1 ∩ V2.
We prove the intermediate claim HWopen: W ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx U1 HU1 V2 HV2).
We prove the intermediate claim HWne: W ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty W p (binintersectI U1 V2 p HpU1 HpV2)).
We prove the intermediate claim HWmeet: W ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx W HTx Hdense HWopen HWne).
We prove the intermediate claim Hexd: ∃d : set, d ∈ W ∩ D.
An exact proof term for the current goal is (nonempty_has_element (W ∩ D) HWmeet).
Apply Hexd to the current goal.
Let d be given.
Assume HdWD: d ∈ W ∩ D.
We prove the intermediate claim HdW: d ∈ W.
An exact proof term for the current goal is (binintersectE1 W D d HdWD).
We prove the intermediate claim HdD: d ∈ D.
An exact proof term for the current goal is (binintersectE2 W D d HdWD).
We prove the intermediate claim HdefW: W = U1 ∩ V2.
Use reflexivity.
We prove the intermediate claim HdWV: d ∈ U1 ∩ V2.
rewrite the current goal using HdefW (from right to left).
An exact proof term for the current goal is HdW.
We prove the intermediate claim HdU1: d ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 V2 d HdWV).
We prove the intermediate claim HdV2: d ∈ V2.
An exact proof term for the current goal is (binintersectE2 U1 V2 d HdWV).
We prove the intermediate claim HUofA: Uof A = U1.
We prove the intermediate claim HdefU: Uof A = (UV A) 0.
Use reflexivity.
rewrite the current goal using HdefU (from left to right).
rewrite the current goal using HUV_A (from left to right).
rewrite the current goal using (tuple_pair U1 V1) (from right to left).
An exact proof term for the current goal is (pair_ap_0 U1 V1).
We prove the intermediate claim HUofB: Uof B = U2.
We prove the intermediate claim HdefU: Uof B = (UV B) 0.
Use reflexivity.
rewrite the current goal using HdefU (from left to right).
rewrite the current goal using HUV_B (from left to right).
rewrite the current goal using (tuple_pair U2 V2) (from right to left).
An exact proof term for the current goal is (pair_ap_0 U2 V2).
We prove the intermediate claim HVofB: Vof B = V2.
We prove the intermediate claim HdefV: Vof B = (UV B) 1.
Use reflexivity.
rewrite the current goal using HdefV (from left to right).
rewrite the current goal using HUV_B (from left to right).
rewrite the current goal using (tuple_pair U2 V2) (from right to left).
An exact proof term for the current goal is (pair_ap_1 U2 V2).
We prove the intermediate claim HdthetaA: d ∈ theta A.
We prove the intermediate claim HdefTheta: theta A = D ∩ (Uof A).
Use reflexivity.
rewrite the current goal using HdefTheta (from left to right).
rewrite the current goal using HUofA (from left to right).
An exact proof term for the current goal is (binintersectI D U1 d HdD HdU1).
We prove the intermediate claim HdNotUofB: d ∉ Uof B.
Assume HdUofB: d ∈ Uof B.
We prove the intermediate claim HdU2: d ∈ U2.
rewrite the current goal using HUofB (from right to left).
An exact proof term for the current goal is HdUofB.
We prove the intermediate claim HdUV0: d ∈ U2 ∩ V2.
An exact proof term for the current goal is (binintersectI U2 V2 d HdU2 HdV2).
We prove the intermediate claim HdEmpty: d ∈ Empty.
rewrite the current goal using HdisjB (from right to left).
An exact proof term for the current goal is HdUV0.
An exact proof term for the current goal is (EmptyE d HdEmpty False).
We prove the intermediate claim HdNotThetaB: d ∉ theta B.
Assume HdthetaB: d ∈ theta B.
We prove the intermediate claim HdefThetaB: theta B = D ∩ (Uof B).
Use reflexivity.
We prove the intermediate claim HdthetaB0: d ∈ D ∩ (Uof B).
rewrite the current goal using HdefThetaB (from right to left).
An exact proof term for the current goal is HdthetaB.
We prove the intermediate claim HdUofB: d ∈ Uof B.
An exact proof term for the current goal is (binintersectE2 D (Uof B) d HdthetaB0).
An exact proof term for the current goal is (HdNotUofB HdUofB).
We prove the intermediate claim HdthetaB0: d ∈ theta B.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HdthetaA.
An exact proof term for the current goal is (FalseE (HdNotThetaB HdthetaB0) (p ∈ B)).
We prove the intermediate claim HBA: B ⊆ A.
Let p be given.
Assume HpB: p ∈ B.
We will prove p ∈ A.
Apply xm (p ∈ A) to the current goal.
Assume HpA: p ∈ A.
An exact proof term for the current goal is HpA.
Assume HpNotA: p ∉ A.
We will prove p ∈ A.
We prove the intermediate claim HAsubL: A ⊆ L.
An exact proof term for the current goal is (PowerE L A HA).
We prove the intermediate claim HBsubL: B ⊆ L.
An exact proof term for the current goal is (PowerE L B HB).
We prove the intermediate claim HpL: p ∈ L.
An exact proof term for the current goal is (HBsubL p HpB).
We prove the intermediate claim HpLA: p ∈ (L ∖ A).
An exact proof term for the current goal is (setminusI L A p HpL HpNotA).
We prove the intermediate claim HexA: ∃U1 V1 : set, UV A = (U1,V1) ∧ (U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty).
An exact proof term for the current goal is (HUV_ok A HA).
We prove the intermediate claim HexB: ∃U2 V2 : set, UV B = (U2,V2) ∧ (U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty).
An exact proof term for the current goal is (HUV_ok B HB).
Apply HexA to the current goal.
Let U1 be given.
Assume HexV1.
Apply HexV1 to the current goal.
Let V1 be given.
Assume HpackA.
Apply HexB to the current goal.
Let U2 be given.
Assume HexV2.
Apply HexV2 to the current goal.
Let V2 be given.
Assume HpackB.
We prove the intermediate claim HUV_A: UV A = (U1,V1).
An exact proof term for the current goal is (andEL (UV A = (U1,V1)) (U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty) HpackA).
We prove the intermediate claim HUV_B: UV B = (U2,V2).
An exact proof term for the current goal is (andEL (UV B = (U2,V2)) (U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty) HpackB).
We prove the intermediate claim HpropsA: U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (andER (UV A = (U1,V1)) (U1 ∈ Tx ∧ V1 ∈ Tx ∧ A ⊆ U1 ∧ (L ∖ A) ⊆ V1 ∧ U1 ∩ V1 = Empty) HpackA).
We prove the intermediate claim HpropsB: U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty.
An exact proof term for the current goal is (andER (UV B = (U2,V2)) (U2 ∈ Tx ∧ V2 ∈ Tx ∧ B ⊆ U2 ∧ (L ∖ B) ⊆ V2 ∧ U2 ∩ V2 = Empty) HpackB).
We prove the intermediate claim HleftA: ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ∧ (L ∖ A) ⊆ V1.
An exact proof term for the current goal is (andEL (((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ∧ (L ∖ A) ⊆ V1) (U1 ∩ V1 = Empty) HpropsA).
We prove the intermediate claim HUV1pair: (U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1.
An exact proof term for the current goal is (andEL ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ((L ∖ A) ⊆ V1) HleftA).
We prove the intermediate claim HU1V1: U1 ∈ Tx ∧ V1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ V1 ∈ Tx) (A ⊆ U1) HUV1pair).
We prove the intermediate claim HV1: V1 ∈ Tx.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (V1 ∈ Tx) HU1V1).
We prove the intermediate claim HLBsubV1: (L ∖ A) ⊆ V1.
An exact proof term for the current goal is (andER ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ((L ∖ A) ⊆ V1) HleftA).
We prove the intermediate claim HdisjA: U1 ∩ V1 = Empty.
An exact proof term for the current goal is (andER (((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ A ⊆ U1) ∧ (L ∖ A) ⊆ V1) (U1 ∩ V1 = Empty) HpropsA).
We prove the intermediate claim HleftB: ((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ∧ (L ∖ B) ⊆ V2.
An exact proof term for the current goal is (andEL (((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ∧ (L ∖ B) ⊆ V2) (U2 ∩ V2 = Empty) HpropsB).
We prove the intermediate claim HUV2pair: (U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2.
An exact proof term for the current goal is (andEL ((U2 ∈ Tx ∧ V2 ∈ Tx) ∧ B ⊆ U2) ((L ∖ B) ⊆ V2) HleftB).
We prove the intermediate claim HU2V2: U2 ∈ Tx ∧ V2 ∈ Tx.
An exact proof term for the current goal is (andEL (U2 ∈ Tx ∧ V2 ∈ Tx) (B ⊆ U2) HUV2pair).
We prove the intermediate claim HU2: U2 ∈ Tx.
An exact proof term for the current goal is (andEL (U2 ∈ Tx) (V2 ∈ Tx) HU2V2).
We prove the intermediate claim HBsubU2: B ⊆ U2.
An exact proof term for the current goal is (andER (U2 ∈ Tx ∧ V2 ∈ Tx) (B ⊆ U2) HUV2pair).
We prove the intermediate claim HpU2: p ∈ U2.
An exact proof term for the current goal is (HBsubU2 p HpB).
We prove the intermediate claim HpV1: p ∈ V1.
An exact proof term for the current goal is (HLBsubV1 p HpLA).
Set W to be the term U2 ∩ V1.
We prove the intermediate claim HWopen: W ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_axiom X Tx HTx U2 HU2 V1 HV1).
We prove the intermediate claim HWne: W ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty W p (binintersectI U2 V1 p HpU2 HpV1)).
We prove the intermediate claim HWmeet: W ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx W HTx Hdense HWopen HWne).
We prove the intermediate claim Hexd: ∃d : set, d ∈ W ∩ D.
An exact proof term for the current goal is (nonempty_has_element (W ∩ D) HWmeet).
Apply Hexd to the current goal.
Let d be given.
Assume HdWD: d ∈ W ∩ D.
We prove the intermediate claim HdW: d ∈ W.
An exact proof term for the current goal is (binintersectE1 W D d HdWD).
We prove the intermediate claim HdD: d ∈ D.
An exact proof term for the current goal is (binintersectE2 W D d HdWD).
We prove the intermediate claim HdefW: W = U2 ∩ V1.
Use reflexivity.
We prove the intermediate claim HdWV: d ∈ U2 ∩ V1.
rewrite the current goal using HdefW (from right to left).
An exact proof term for the current goal is HdW.
We prove the intermediate claim HdU2: d ∈ U2.
An exact proof term for the current goal is (binintersectE1 U2 V1 d HdWV).
We prove the intermediate claim HdV1: d ∈ V1.
An exact proof term for the current goal is (binintersectE2 U2 V1 d HdWV).
We prove the intermediate claim HUofA: Uof A = U1.
We prove the intermediate claim HdefU: Uof A = (UV A) 0.
Use reflexivity.
rewrite the current goal using HdefU (from left to right).
rewrite the current goal using HUV_A (from left to right).
rewrite the current goal using (tuple_pair U1 V1) (from right to left).
An exact proof term for the current goal is (pair_ap_0 U1 V1).
We prove the intermediate claim HUofB: Uof B = U2.
We prove the intermediate claim HdefU: Uof B = (UV B) 0.
Use reflexivity.
rewrite the current goal using HdefU (from left to right).
rewrite the current goal using HUV_B (from left to right).
rewrite the current goal using (tuple_pair U2 V2) (from right to left).
An exact proof term for the current goal is (pair_ap_0 U2 V2).
We prove the intermediate claim HdthetaB: d ∈ theta B.
We prove the intermediate claim HdefTheta: theta B = D ∩ (Uof B).
Use reflexivity.
rewrite the current goal using HdefTheta (from left to right).
rewrite the current goal using HUofB (from left to right).
An exact proof term for the current goal is (binintersectI D U2 d HdD HdU2).
We prove the intermediate claim HdNotUofA: d ∉ Uof A.
Assume HdUofA: d ∈ Uof A.
We prove the intermediate claim HdU1: d ∈ U1.
rewrite the current goal using HUofA (from right to left).
An exact proof term for the current goal is HdUofA.
We prove the intermediate claim HdUV0: d ∈ U1 ∩ V1.
An exact proof term for the current goal is (binintersectI U1 V1 d HdU1 HdV1).
We prove the intermediate claim HdEmpty: d ∈ Empty.
rewrite the current goal using HdisjA (from right to left).
An exact proof term for the current goal is HdUV0.
An exact proof term for the current goal is (EmptyE d HdEmpty False).
We prove the intermediate claim HdNotThetaA: d ∉ theta A.
Assume HdthetaA: d ∈ theta A.
We prove the intermediate claim HdUofA: d ∈ Uof A.
An exact proof term for the current goal is (binintersectE2 D (Uof A) d HdthetaA).
An exact proof term for the current goal is (HdNotUofA HdUofA).
We prove the intermediate claim HdthetaA0: d ∈ theta A.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HdthetaB.
An exact proof term for the current goal is (FalseE (HdNotThetaA HdthetaA0) (p ∈ A)).
An exact proof term for the current goal is (set_ext A B HAB HBA).
Apply HcountD to the current goal.
Let fD be given.
Assume HfD: inj D ω fD.
Set Pow_fD to be the term λS : set ⇒ {fD x|x ∈ S}.
We prove the intermediate claim HpowD: inj (𝒫 D) (𝒫 ω) Pow_fD.
An exact proof term for the current goal is (inj_Power_image D ω fD HfD).
We prove the intermediate claim HeqR: equip real (𝒫 ω).
An exact proof term for the current goal is equip_real_Power_omega.
We prove the intermediate claim HeqRsym: equip (𝒫 ω) real.
An exact proof term for the current goal is (equip_sym real (𝒫 ω) HeqR).
We prove the intermediate claim HatleastpPow: atleastp (𝒫 ω) real.
An exact proof term for the current goal is (equip_atleastp (𝒫 ω) real HeqRsym).
Apply HatleastpPow to the current goal.
Let h0 be given.
Assume Hh0: inj (𝒫 ω) real h0.
We prove the intermediate claim HlineDef: Sorgenfrey_line = real.
We prove the intermediate claim H1: Sorgenfrey_line = R.
Use reflexivity.
We prove the intermediate claim H2: R = real.
Use reflexivity.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hh0line: inj (𝒫 ω) Sorgenfrey_line h0.
rewrite the current goal using HlineDef (from left to right).
An exact proof term for the current goal is Hh0.
We prove the intermediate claim HinjLineL: inj Sorgenfrey_line L (λx : set ⇒ (x,minus_SNo x)).
Apply (injI Sorgenfrey_line L (λx : set ⇒ (x,minus_SNo x))) to the current goal.
Let x be given.
Assume Hx: x ∈ Sorgenfrey_line.
We will prove (x,minus_SNo x) ∈ L.
An exact proof term for the current goal is (ReplI Sorgenfrey_line (λx0 : set ⇒ (x0,minus_SNo x0)) x Hx).
Let x1 be given.
Assume Hx1: x1 ∈ Sorgenfrey_line.
Let x2 be given.
Assume Hx2: x2 ∈ Sorgenfrey_line.
Assume Heq: (x1,minus_SNo x1) = (x2,minus_SNo x2).
We will prove x1 = x2.
We prove the intermediate claim H0: (x1,minus_SNo x1) 0 = (x2,minus_SNo x2) 0.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hx10: (x1,minus_SNo x1) 0 = x1.
rewrite the current goal using (tuple_pair x1 (minus_SNo x1)) (from right to left).
An exact proof term for the current goal is (pair_ap_0 x1 (minus_SNo x1)).
We prove the intermediate claim Hx20: (x2,minus_SNo x2) 0 = x2.
rewrite the current goal using (tuple_pair x2 (minus_SNo x2)) (from right to left).
An exact proof term for the current goal is (pair_ap_0 x2 (minus_SNo x2)).
rewrite the current goal using Hx10 (from right to left) at position 1.
rewrite the current goal using Hx20 (from right to left).
An exact proof term for the current goal is H0.
We prove the intermediate claim HinjPowL: inj (𝒫 ω) L (λS : set ⇒ (λx : set ⇒ (x,minus_SNo x)) (h0 S)).
An exact proof term for the current goal is (inj_comp (𝒫 ω) Sorgenfrey_line L h0 (λx : set ⇒ (x,minus_SNo x)) Hh0line HinjLineL).
Set Pow_h to be the term λS : set ⇒ {(λS0 : set ⇒ (λx : set ⇒ (x,minus_SNo x)) (h0 S0)) x|x ∈ S}.
We prove the intermediate claim HpowL: inj (𝒫 (𝒫 ω)) (𝒫 L) Pow_h.
An exact proof term for the current goal is (inj_Power_image (𝒫 ω) L (λS0 : set ⇒ (λx : set ⇒ (x,minus_SNo x)) (h0 S0)) HinjPowL).
Set mid to be the term λS : set ⇒ theta (Pow_h S).
We prove the intermediate claim Hmid: inj (𝒫 (𝒫 ω)) (𝒫 D) mid.
An exact proof term for the current goal is (inj_comp (𝒫 (𝒫 ω)) (𝒫 L) (𝒫 D) Pow_h theta HpowL Htheta_inj).
Set final to be the term λS : set ⇒ Pow_fD (mid S).
We prove the intermediate claim Hfinal: inj (𝒫 (𝒫 ω)) (𝒫 ω) final.
An exact proof term for the current goal is (inj_comp (𝒫 (𝒫 ω)) (𝒫 D) (𝒫 ω) mid Pow_fD Hmid HpowD).
An exact proof term for the current goal is ((form100_63_injCantor (𝒫 ω) final) Hfinal).
∎