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

Proof

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