Theorem onint1 32448

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

Assertion

Ref	Expression
onint1	⊢ (On ∩ Fre) = {1𝑜, 2𝑜}

Proof of Theorem onint1

Dummy variables 𝑗 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3796	. . . . 5 ⊢ (𝑗 ∈ (On ∩ Fre) ↔ (𝑗 ∈ On ∧ 𝑗 ∈ Fre))
2		eqid 2622	. . . . . . . . . . 11 ⊢ ∪ 𝑗 = ∪ 𝑗
3	2	ist1 21125	. . . . . . . . . 10 ⊢ (𝑗 ∈ Fre ↔ (𝑗 ∈ Top ∧ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)))
4	3	simprbi 480	. . . . . . . . 9 ⊢ (𝑗 ∈ Fre → ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))
5		onelon 5748	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ On ∧ (∪ 𝑗 ∖ {∅}) ∈ 𝑗) → (∪ 𝑗 ∖ {∅}) ∈ On)
6	5	ex 450	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ On → ((∪ 𝑗 ∖ {∅}) ∈ 𝑗 → (∪ 𝑗 ∖ {∅}) ∈ On))
7		neldifsnd 4322	. . . . . . . . . . . . . . . . 17 ⊢ (2𝑜 ∈ 𝑗 → ¬ ∅ ∈ (∪ 𝑗 ∖ {∅}))
8		p0ex 4853	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {∅} ∈ V
9	8	prid2 4298	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅} ∈ {∅, {∅}}
10		df2o2 7574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2𝑜 = {∅, {∅}}
11	9, 10	eleqtrri 2700	. . . . . . . . . . . . . . . . . . . 20 ⊢ {∅} ∈ 2𝑜
12		elunii 4441	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({∅} ∈ 2𝑜 ∧ 2𝑜 ∈ 𝑗) → {∅} ∈ ∪ 𝑗)
13	11, 12	mpan 706	. . . . . . . . . . . . . . . . . . 19 ⊢ (2𝑜 ∈ 𝑗 → {∅} ∈ ∪ 𝑗)
14		df1o2 7572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1𝑜 = {∅}
15		1on 7567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1𝑜 ∈ On
16	14, 15	eqeltrri 2698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅} ∈ On
17	16	onirri 5834	. . . . . . . . . . . . . . . . . . . 20 ⊢ ¬ {∅} ∈ {∅}
18	17	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (2𝑜 ∈ 𝑗 → ¬ {∅} ∈ {∅})
19	13, 18	eldifd 3585	. . . . . . . . . . . . . . . . . 18 ⊢ (2𝑜 ∈ 𝑗 → {∅} ∈ (∪ 𝑗 ∖ {∅}))
20		ne0i 3921	. . . . . . . . . . . . . . . . . 18 ⊢ ({∅} ∈ (∪ 𝑗 ∖ {∅}) → (∪ 𝑗 ∖ {∅}) ≠ ∅)
21	19, 20	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (2𝑜 ∈ 𝑗 → (∪ 𝑗 ∖ {∅}) ≠ ∅)
22	7, 21	2thd 255	. . . . . . . . . . . . . . . 16 ⊢ (2𝑜 ∈ 𝑗 → (¬ ∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
23		nbbn 373	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅) ↔ ¬ (∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
24	22, 23	sylib 208	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 ∈ 𝑗 → ¬ (∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
25		on0eln0 5780	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑗 ∖ {∅}) ∈ On → (∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
26	24, 25	nsyl 135	. . . . . . . . . . . . . 14 ⊢ (2𝑜 ∈ 𝑗 → ¬ (∪ 𝑗 ∖ {∅}) ∈ On)
27	6, 26	nsyli 155	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ On → (2𝑜 ∈ 𝑗 → ¬ (∪ 𝑗 ∖ {∅}) ∈ 𝑗))
28	27	imp 445	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → ¬ (∪ 𝑗 ∖ {∅}) ∈ 𝑗)
29		0ex 4790	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
30	29	prid1 4297	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅, {∅}}
31	30, 10	eleqtrri 2700	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ 2𝑜
32		elunii 4441	. . . . . . . . . . . . . . . 16 ⊢ ((∅ ∈ 2𝑜 ∧ 2𝑜 ∈ 𝑗) → ∅ ∈ ∪ 𝑗)
33	31, 32	mpan 706	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 ∈ 𝑗 → ∅ ∈ ∪ 𝑗)
34	33	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → ∅ ∈ ∪ 𝑗)
35		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → 𝑎 = ∅)
36	35	sneqd 4189	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → {𝑎} = {∅})
37	36	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → ({𝑎} ∈ (Clsd‘𝑗) ↔ {∅} ∈ (Clsd‘𝑗)))
38	34, 37	rspcdv 3312	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → {∅} ∈ (Clsd‘𝑗)))
39	2	cldopn 20835	. . . . . . . . . . . . 13 ⊢ ({∅} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗)
40	38, 39	syl6 35	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗))
41	28, 40	mtod 189	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → ¬ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))
42	41	ex 450	. . . . . . . . . 10 ⊢ (𝑗 ∈ On → (2𝑜 ∈ 𝑗 → ¬ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)))
43	42	con2d 129	. . . . . . . . 9 ⊢ (𝑗 ∈ On → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → ¬ 2𝑜 ∈ 𝑗))
44	4, 43	syl5 34	. . . . . . . 8 ⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → ¬ 2𝑜 ∈ 𝑗))
45		2on 7568	. . . . . . . . 9 ⊢ 2𝑜 ∈ On
46		ontri1 5757	. . . . . . . . . 10 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ On) → (𝑗 ⊆ 2𝑜 ↔ ¬ 2𝑜 ∈ 𝑗))
47		onsssuc 5813	. . . . . . . . . 10 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ On) → (𝑗 ⊆ 2𝑜 ↔ 𝑗 ∈ suc 2𝑜))
48	46, 47	bitr3d 270	. . . . . . . . 9 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ On) → (¬ 2𝑜 ∈ 𝑗 ↔ 𝑗 ∈ suc 2𝑜))
49	45, 48	mpan2 707	. . . . . . . 8 ⊢ (𝑗 ∈ On → (¬ 2𝑜 ∈ 𝑗 ↔ 𝑗 ∈ suc 2𝑜))
50	44, 49	sylibd 229	. . . . . . 7 ⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → 𝑗 ∈ suc 2𝑜))
51	50	imp 445	. . . . . 6 ⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ suc 2𝑜)
52		0ntop 20710	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ Top
53		t1top 21134	. . . . . . . . . 10 ⊢ (∅ ∈ Fre → ∅ ∈ Top)
54	52, 53	mto 188	. . . . . . . . 9 ⊢ ¬ ∅ ∈ Fre
55		nelneq 2725	. . . . . . . . 9 ⊢ ((𝑗 ∈ Fre ∧ ¬ ∅ ∈ Fre) → ¬ 𝑗 = ∅)
56	54, 55	mpan2 707	. . . . . . . 8 ⊢ (𝑗 ∈ Fre → ¬ 𝑗 = ∅)
57		elsni 4194	. . . . . . . 8 ⊢ (𝑗 ∈ {∅} → 𝑗 = ∅)
58	56, 57	nsyl 135	. . . . . . 7 ⊢ (𝑗 ∈ Fre → ¬ 𝑗 ∈ {∅})
59	58	adantl 482	. . . . . 6 ⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → ¬ 𝑗 ∈ {∅})
60	51, 59	eldifd 3585	. . . . 5 ⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ (suc 2𝑜 ∖ {∅}))
61	1, 60	sylbi 207	. . . 4 ⊢ (𝑗 ∈ (On ∩ Fre) → 𝑗 ∈ (suc 2𝑜 ∖ {∅}))
62	61	ssriv 3607	. . 3 ⊢ (On ∩ Fre) ⊆ (suc 2𝑜 ∖ {∅})
63		df-suc 5729	. . . . . 6 ⊢ suc 2𝑜 = (2𝑜 ∪ {2𝑜})
64	63	difeq1i 3724	. . . . 5 ⊢ (suc 2𝑜 ∖ {∅}) = ((2𝑜 ∪ {2𝑜}) ∖ {∅})
65		difundir 3880	. . . . 5 ⊢ ((2𝑜 ∪ {2𝑜}) ∖ {∅}) = ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅}))
66	64, 65	eqtri 2644	. . . 4 ⊢ (suc 2𝑜 ∖ {∅}) = ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅}))
67		df-pr 4180	. . . . 5 ⊢ {1𝑜, 2𝑜} = ({1𝑜} ∪ {2𝑜})
68		df2o3 7573	. . . . . . . . 9 ⊢ 2𝑜 = {∅, 1𝑜}
69		df-pr 4180	. . . . . . . . 9 ⊢ {∅, 1𝑜} = ({∅} ∪ {1𝑜})
70	68, 69	eqtri 2644	. . . . . . . 8 ⊢ 2𝑜 = ({∅} ∪ {1𝑜})
71	70	difeq1i 3724	. . . . . . 7 ⊢ (2𝑜 ∖ {∅}) = (({∅} ∪ {1𝑜}) ∖ {∅})
72		difundir 3880	. . . . . . 7 ⊢ (({∅} ∪ {1𝑜}) ∖ {∅}) = (({∅} ∖ {∅}) ∪ ({1𝑜} ∖ {∅}))
73		difid 3948	. . . . . . . . 9 ⊢ ({∅} ∖ {∅}) = ∅
74		1n0 7575	. . . . . . . . . . . 12 ⊢ 1𝑜 ≠ ∅
75		disjsn2 4247	. . . . . . . . . . . 12 ⊢ (1𝑜 ≠ ∅ → ({1𝑜} ∩ {∅}) = ∅)
76	74, 75	ax-mp 5	. . . . . . . . . . 11 ⊢ ({1𝑜} ∩ {∅}) = ∅
77	76	difeq2i 3725	. . . . . . . . . 10 ⊢ ({1𝑜} ∖ ({1𝑜} ∩ {∅})) = ({1𝑜} ∖ ∅)
78		difin 3861	. . . . . . . . . 10 ⊢ ({1𝑜} ∖ ({1𝑜} ∩ {∅})) = ({1𝑜} ∖ {∅})
79		dif0 3950	. . . . . . . . . 10 ⊢ ({1𝑜} ∖ ∅) = {1𝑜}
80	77, 78, 79	3eqtr3i 2652	. . . . . . . . 9 ⊢ ({1𝑜} ∖ {∅}) = {1𝑜}
81	73, 80	uneq12i 3765	. . . . . . . 8 ⊢ (({∅} ∖ {∅}) ∪ ({1𝑜} ∖ {∅})) = (∅ ∪ {1𝑜})
82		uncom 3757	. . . . . . . 8 ⊢ (∅ ∪ {1𝑜}) = ({1𝑜} ∪ ∅)
83		un0 3967	. . . . . . . 8 ⊢ ({1𝑜} ∪ ∅) = {1𝑜}
84	81, 82, 83	3eqtri 2648	. . . . . . 7 ⊢ (({∅} ∖ {∅}) ∪ ({1𝑜} ∖ {∅})) = {1𝑜}
85	71, 72, 84	3eqtri 2648	. . . . . 6 ⊢ (2𝑜 ∖ {∅}) = {1𝑜}
86		2on0 7569	. . . . . . . . 9 ⊢ 2𝑜 ≠ ∅
87		disjsn2 4247	. . . . . . . . 9 ⊢ (2𝑜 ≠ ∅ → ({2𝑜} ∩ {∅}) = ∅)
88	86, 87	ax-mp 5	. . . . . . . 8 ⊢ ({2𝑜} ∩ {∅}) = ∅
89	88	difeq2i 3725	. . . . . . 7 ⊢ ({2𝑜} ∖ ({2𝑜} ∩ {∅})) = ({2𝑜} ∖ ∅)
90		difin 3861	. . . . . . 7 ⊢ ({2𝑜} ∖ ({2𝑜} ∩ {∅})) = ({2𝑜} ∖ {∅})
91		dif0 3950	. . . . . . 7 ⊢ ({2𝑜} ∖ ∅) = {2𝑜}
92	89, 90, 91	3eqtr3i 2652	. . . . . 6 ⊢ ({2𝑜} ∖ {∅}) = {2𝑜}
93	85, 92	uneq12i 3765	. . . . 5 ⊢ ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅})) = ({1𝑜} ∪ {2𝑜})
94	67, 93	eqtr4i 2647	. . . 4 ⊢ {1𝑜, 2𝑜} = ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅}))
95	66, 94	eqtr4i 2647	. . 3 ⊢ (suc 2𝑜 ∖ {∅}) = {1𝑜, 2𝑜}
96	62, 95	sseqtri 3637	. 2 ⊢ (On ∩ Fre) ⊆ {1𝑜, 2𝑜}
97		ssoninhaus 32447	. . 3 ⊢ {1𝑜, 2𝑜} ⊆ (On ∩ Haus)
98		haust1 21156	. . . . 5 ⊢ (𝑗 ∈ Haus → 𝑗 ∈ Fre)
99	98	ssriv 3607	. . . 4 ⊢ Haus ⊆ Fre
100		sslin 3839	. . . 4 ⊢ (Haus ⊆ Fre → (On ∩ Haus) ⊆ (On ∩ Fre))
101	99, 100	ax-mp 5	. . 3 ⊢ (On ∩ Haus) ⊆ (On ∩ Fre)
102	97, 101	sstri 3612	. 2 ⊢ {1𝑜, 2𝑜} ⊆ (On ∩ Fre)
103	96, 102	eqssi 3619	1 ⊢ (On ∩ Fre) = {1𝑜, 2𝑜}

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  {csn 4177  {cpr 4179  ∪ cuni 4436  Oncon0 5723  suc csuc 5725  ‘cfv 5888  1_𝑜c1o 7553  2_𝑜c2o 7554  Topctop 20698  Clsdccld 20820  Frect1 21111  Hauscha 21112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-1o 7560  df-2o 7561  df-topgen 16104  df-top 20699  df-topon 20716  df-cld 20823  df-t1 21118  df-haus 21119

This theorem is referenced by:  oninhaus  32449