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 i^i Fre ) = { 1o , 2o }

Proof

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