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∈⋃ja∈Clsd⁡j
4 3 simprbi ⊢j∈Fre→∀a∈⋃ja∈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∈⋃ja∈Clsd⁡j→∅∈Clsd⁡j
38 2 cldopn ⊢∅∈Clsd⁡j→⋃j∖∅∈j
39 37 38 syl6 ⊢j∈On∧2𝑜∈j→∀a∈⋃ja∈Clsd⁡j→⋃j∖∅∈j
40 27 39 mtod ⊢j∈On∧2𝑜∈j→¬∀a∈⋃ja∈Clsd⁡j
41 40 ex ⊢j∈On→2𝑜∈j→¬∀a∈⋃ja∈Clsd⁡j
42 41 con2d ⊢j∈On→∀a∈⋃ja∈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𝑜