Metamath Proof Explorer


Theorem onint1

Description: The ordinal T_1 spaces are 1o and 2o , proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015)

Ref Expression
Assertion onint1 On Fre = 1 𝑜 2 𝑜

Proof

Step Hyp Ref Expression
1 elin j On Fre j On j Fre
2 eqid j = j
3 2 ist1 j Fre j Top a j a Clsd j
4 3 simprbi j Fre a j a Clsd j
5 onelon j On j j j On
6 5 ex j On j j j On
7 neldifsnd 2 𝑜 j ¬ j
8 p0ex V
9 8 prid2
10 df2o2 2 𝑜 =
11 9 10 eleqtrri 2 𝑜
12 elunii 2 𝑜 2 𝑜 j j
13 11 12 mpan 2 𝑜 j j
14 df1o2 1 𝑜 =
15 1on 1 𝑜 On
16 14 15 eqeltrri On
17 16 onirri ¬
18 17 a1i 2 𝑜 j ¬
19 13 18 eldifd 2 𝑜 j j
20 19 ne0d 2 𝑜 j j
21 7 20 2thd 2 𝑜 j ¬ j j
22 nbbn ¬ j j ¬ j j
23 21 22 sylib 2 𝑜 j ¬ j j
24 on0eln0 j On j j
25 23 24 nsyl 2 𝑜 j ¬ j On
26 6 25 nsyli j On 2 𝑜 j ¬ j j
27 26 imp j On 2 𝑜 j ¬ j j
28 0ex V
29 28 prid1
30 29 10 eleqtrri 2 𝑜
31 elunii 2 𝑜 2 𝑜 j j
32 30 31 mpan 2 𝑜 j j
33 32 adantl j On 2 𝑜 j j
34 simpr j On 2 𝑜 j a = a =
35 34 sneqd j On 2 𝑜 j a = a =
36 35 eleq1d j On 2 𝑜 j a = a Clsd j Clsd j
37 33 36 rspcdv j On 2 𝑜 j a j a Clsd j Clsd j
38 2 cldopn Clsd j j j
39 37 38 syl6 j On 2 𝑜 j a j a Clsd j j j
40 27 39 mtod j On 2 𝑜 j ¬ a j a Clsd j
41 40 ex j On 2 𝑜 j ¬ a j a Clsd j
42 41 con2d j On a j a Clsd j ¬ 2 𝑜 j
43 4 42 syl5 j On j Fre ¬ 2 𝑜 j
44 2on 2 𝑜 On
45 ontri1 j On 2 𝑜 On j 2 𝑜 ¬ 2 𝑜 j
46 onsssuc j On 2 𝑜 On j 2 𝑜 j suc 2 𝑜
47 45 46 bitr3d j On 2 𝑜 On ¬ 2 𝑜 j j suc 2 𝑜
48 44 47 mpan2 j On ¬ 2 𝑜 j j suc 2 𝑜
49 43 48 sylibd j On j Fre j suc 2 𝑜
50 49 imp j On j Fre j suc 2 𝑜
51 0ntop ¬ Top
52 t1top Fre Top
53 51 52 mto ¬ Fre
54 nelneq j Fre ¬ Fre ¬ j =
55 53 54 mpan2 j Fre ¬ j =
56 elsni j j =
57 55 56 nsyl j Fre ¬ j
58 57 adantl j On j Fre ¬ j
59 50 58 eldifd j On j Fre j suc 2 𝑜
60 1 59 sylbi j On Fre j suc 2 𝑜
61 60 ssriv On Fre suc 2 𝑜
62 df-suc suc 2 𝑜 = 2 𝑜 2 𝑜
63 62 difeq1i suc 2 𝑜 = 2 𝑜 2 𝑜
64 difundir 2 𝑜 2 𝑜 = 2 𝑜 2 𝑜
65 63 64 eqtri suc 2 𝑜 = 2 𝑜 2 𝑜
66 df-pr 1 𝑜 2 𝑜 = 1 𝑜 2 𝑜
67 df2o3 2 𝑜 = 1 𝑜
68 df-pr 1 𝑜 = 1 𝑜
69 67 68 eqtri 2 𝑜 = 1 𝑜
70 69 difeq1i 2 𝑜 = 1 𝑜
71 difundir 1 𝑜 = 1 𝑜
72 difid =
73 1n0 1 𝑜
74 disjsn2 1 𝑜 1 𝑜 =
75 73 74 ax-mp 1 𝑜 =
76 75 difeq2i 1 𝑜 1 𝑜 = 1 𝑜
77 difin 1 𝑜 1 𝑜 = 1 𝑜
78 dif0 1 𝑜 = 1 𝑜
79 76 77 78 3eqtr3i 1 𝑜 = 1 𝑜
80 72 79 uneq12i 1 𝑜 = 1 𝑜
81 uncom 1 𝑜 = 1 𝑜
82 un0 1 𝑜 = 1 𝑜
83 80 81 82 3eqtri 1 𝑜 = 1 𝑜
84 70 71 83 3eqtri 2 𝑜 = 1 𝑜
85 2on0 2 𝑜
86 disjsn2 2 𝑜 2 𝑜 =
87 85 86 ax-mp 2 𝑜 =
88 87 difeq2i 2 𝑜 2 𝑜 = 2 𝑜
89 difin 2 𝑜 2 𝑜 = 2 𝑜
90 dif0 2 𝑜 = 2 𝑜
91 88 89 90 3eqtr3i 2 𝑜 = 2 𝑜
92 84 91 uneq12i 2 𝑜 2 𝑜 = 1 𝑜 2 𝑜
93 66 92 eqtr4i 1 𝑜 2 𝑜 = 2 𝑜 2 𝑜
94 65 93 eqtr4i suc 2 𝑜 = 1 𝑜 2 𝑜
95 61 94 sseqtri On Fre 1 𝑜 2 𝑜
96 ssoninhaus 1 𝑜 2 𝑜 On Haus
97 haust1 j Haus j Fre
98 97 ssriv Haus Fre
99 sslin Haus Fre On Haus On Fre
100 98 99 ax-mp On Haus On Fre
101 96 100 sstri 1 𝑜 2 𝑜 On Fre
102 95 101 eqssi On Fre = 1 𝑜 2 𝑜