Let X, Tx, seq, x and y be given.
Assume HH: Hausdorff_space X Tx.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Hneq: x ≠ y.
Assume Hseq: function_on seq ω X.
Assume Hx: ∀U : set, U ∈ Tx → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
Assume Hy: ∀U : set, U ∈ Tx → y ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
We will prove False.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).
We prove the intermediate claim HSep: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Let x1 and x2 be given.
Assume Hx1: x1 ∈ X.
Assume Hx2: x2 ∈ X.
Assume Hneq12: x1 ≠ x2.
An exact proof term for the current goal is (Hausdorff_space_separation X Tx x1 x2 HH Hx1 Hx2 Hneq12).
We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSep x y HxX HyX Hneq).
Apply HexUV to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty.
Apply HexV to the current goal.
Let V be given.
Assume Hconj: U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (x ∈ U) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U) (y ∈ V) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V) (U ∩ V = Empty) Hconj)))).
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) (andEL (U ∈ Tx ∧ V ∈ Tx) (x ∈ U) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U) (y ∈ V) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V) (U ∩ V = Empty) Hconj)))).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (x ∈ U) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U) (y ∈ V) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V) (U ∩ V = Empty) Hconj))).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U) (y ∈ V) (andEL (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V) (U ∩ V = Empty) Hconj)).
We prove the intermediate claim HUV_empty: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V) (U ∩ V = Empty) Hconj).
We prove the intermediate claim HexNx: ∃Nx : set, Nx ∈ ω ∧ ∀n : set, n ∈ ω → Nx ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (Hx U HU HxU).
Apply HexNx to the current goal.
Let Nx be given.
Assume HNx_and_conv.
We prove the intermediate claim HNx: Nx ∈ ω.
An exact proof term for the current goal is (andEL (Nx ∈ ω) (∀n : set, n ∈ ω → Nx ⊆ n → apply_fun seq n ∈ U) HNx_and_conv).
We prove the intermediate claim Hconv_x: ∀n : set, n ∈ ω → Nx ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (andER (Nx ∈ ω) (∀n : set, n ∈ ω → Nx ⊆ n → apply_fun seq n ∈ U) HNx_and_conv).
We prove the intermediate claim HexNy: ∃Ny : set, Ny ∈ ω ∧ ∀n : set, n ∈ ω → Ny ⊆ n → apply_fun seq n ∈ V.
An exact proof term for the current goal is (Hy V HV HyV).
Apply HexNy to the current goal.
Let Ny be given.
Assume HNy_and_conv.
We prove the intermediate claim HNy: Ny ∈ ω.
An exact proof term for the current goal is (andEL (Ny ∈ ω) (∀n : set, n ∈ ω → Ny ⊆ n → apply_fun seq n ∈ V) HNy_and_conv).
We prove the intermediate claim Hconv_y: ∀n : set, n ∈ ω → Ny ⊆ n → apply_fun seq n ∈ V.
An exact proof term for the current goal is (andER (Ny ∈ ω) (∀n : set, n ∈ ω → Ny ⊆ n → apply_fun seq n ∈ V) HNy_and_conv).
Set N to be the term ordsucc (Nx ∪ Ny).
We prove the intermediate claim HN_omega: N ∈ ω.
We prove the intermediate claim Hmax_omega: Nx ∪ Ny ∈ ω.
Apply (xm (Nx ∈ Ny)) to the current goal.
Assume HNx_in_Ny: Nx ∈ Ny.
We prove the intermediate claim Hmax_eq_Ny: Nx ∪ Ny = Ny.
We prove the intermediate claim HNx_sub_Ny: Nx ⊆ Ny.
We prove the intermediate claim HNy_nat: nat_p Ny.
An exact proof term for the current goal is (omega_nat_p Ny HNy).
We prove the intermediate claim HNy_ord: ordinal Ny.
An exact proof term for the current goal is (nat_p_ordinal Ny HNy_nat).
We prove the intermediate claim HNy_trans: TransSet Ny.
An exact proof term for the current goal is (andEL (TransSet Ny) (∀beta ∈ Ny, TransSet beta) HNy_ord).
An exact proof term for the current goal is (HNy_trans Nx HNx_in_Ny).
Apply set_ext to the current goal.
We prove the intermediate claim HNy_refl: Ny ⊆ Ny.
An exact proof term for the current goal is (Subq_ref Ny).
An exact proof term for the current goal is (binunion_Subq_min Nx Ny Ny HNx_sub_Ny HNy_refl).
An exact proof term for the current goal is (binunion_Subq_2 Nx Ny).
rewrite the current goal using Hmax_eq_Ny (from left to right).
An exact proof term for the current goal is HNy.
Assume HNx_nin_Ny: Nx ∉ Ny.
We prove the intermediate claim HNy_sub_or_eq_Nx: Ny ⊆ Nx.
We prove the intermediate claim HNx_nat: nat_p Nx.
An exact proof term for the current goal is (omega_nat_p Nx HNx).
We prove the intermediate claim HNy_nat: nat_p Ny.
An exact proof term for the current goal is (omega_nat_p Ny HNy).
We prove the intermediate claim HNx_ord: ordinal Nx.
An exact proof term for the current goal is (nat_p_ordinal Nx HNx_nat).
We prove the intermediate claim HNy_ord: ordinal Ny.
An exact proof term for the current goal is (nat_p_ordinal Ny HNy_nat).
We prove the intermediate claim Hcases: Nx ∈ Ny ∨ Ny ⊆ Nx.
An exact proof term for the current goal is (ordinal_In_Or_Subq Nx Ny HNx_ord HNy_ord).
Apply (Hcases (Ny ⊆ Nx)) to the current goal.
Assume HNx_in_Ny: Nx ∈ Ny.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HNx_nin_Ny HNx_in_Ny).
Assume H.
An exact proof term for the current goal is H.
We prove the intermediate claim Hmax_eq_Nx: Nx ∪ Ny = Nx.
Apply set_ext to the current goal.
We prove the intermediate claim HNx_refl: Nx ⊆ Nx.
An exact proof term for the current goal is (Subq_ref Nx).
An exact proof term for the current goal is (binunion_Subq_min Nx Ny Nx HNx_refl HNy_sub_or_eq_Nx).
An exact proof term for the current goal is (binunion_Subq_1 Nx Ny).
rewrite the current goal using Hmax_eq_Nx (from left to right).
An exact proof term for the current goal is HNx.
An exact proof term for the current goal is (omega_ordsucc (Nx ∪ Ny) Hmax_omega).
We prove the intermediate claim HNx_sub_N: Nx ⊆ N.
We prove the intermediate claim HNx_sub_union: Nx ⊆ Nx ∪ Ny.
An exact proof term for the current goal is (binunion_Subq_1 Nx Ny).
We prove the intermediate claim Hunion_sub_ordsucc: Nx ∪ Ny ⊆ ordsucc (Nx ∪ Ny).
An exact proof term for the current goal is (ordsuccI1 (Nx ∪ Ny)).
An exact proof term for the current goal is (Subq_tra Nx (Nx ∪ Ny) (ordsucc (Nx ∪ Ny)) HNx_sub_union Hunion_sub_ordsucc).
We prove the intermediate claim HNy_sub_N: Ny ⊆ N.
We prove the intermediate claim HNy_sub_union: Ny ⊆ Nx ∪ Ny.
An exact proof term for the current goal is (binunion_Subq_2 Nx Ny).
We prove the intermediate claim Hunion_sub_ordsucc: Nx ∪ Ny ⊆ ordsucc (Nx ∪ Ny).
An exact proof term for the current goal is (ordsuccI1 (Nx ∪ Ny)).
An exact proof term for the current goal is (Subq_tra Ny (Nx ∪ Ny) (ordsucc (Nx ∪ Ny)) HNy_sub_union Hunion_sub_ordsucc).
We prove the intermediate claim Hseq_N_in_U: apply_fun seq N ∈ U.
An exact proof term for the current goal is (Hconv_x N HN_omega HNx_sub_N).
We prove the intermediate claim Hseq_N_in_V: apply_fun seq N ∈ V.
An exact proof term for the current goal is (Hconv_y N HN_omega HNy_sub_N).
We prove the intermediate claim Hseq_N_in_UV: apply_fun seq N ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (apply_fun seq N) Hseq_N_in_U Hseq_N_in_V).
We prove the intermediate claim Hseq_N_in_empty: apply_fun seq N ∈ Empty.
rewrite the current goal using HUV_empty (from right to left).
An exact proof term for the current goal is Hseq_N_in_UV.
An exact proof term for the current goal is (EmptyE (apply_fun seq N) Hseq_N_in_empty False).
∎