Theorem onint1 31618

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 3758	. . . . 5 ⊢ (𝑗 ∈ (On ∩ Fre) ↔ (𝑗 ∈ On ∧ 𝑗 ∈ Fre))
2		eqid 2610	. . . . . . . . . . 11 ⊢ ∪ 𝑗 = ∪ 𝑗
3	2	ist1 20935	. . . . . . . . . 10 ⊢ (𝑗 ∈ Fre ↔ (𝑗 ∈ Top ∧ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)))
4	3	simprbi 479	. . . . . . . . 9 ⊢ (𝑗 ∈ Fre → ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))
5		onelon 5665	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ On ∧ (∪ 𝑗 ∖ {∅}) ∈ 𝑗) → (∪ 𝑗 ∖ {∅}) ∈ On)
6	5	ex 449	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ On → ((∪ 𝑗 ∖ {∅}) ∈ 𝑗 → (∪ 𝑗 ∖ {∅}) ∈ On))
7		neldifsnd 4263	. . . . . . . . . . . . . . . . 17 ⊢ (2𝑜 ∈ 𝑗 → ¬ ∅ ∈ (∪ 𝑗 ∖ {∅}))
8		p0ex 4779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {∅} ∈ V
9	8	prid2 4242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅} ∈ {∅, {∅}}
10		df2o2 7461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2𝑜 = {∅, {∅}}
11	9, 10	eleqtrri 2687	. . . . . . . . . . . . . . . . . . . 20 ⊢ {∅} ∈ 2𝑜
12		elunii 4377	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({∅} ∈ 2𝑜 ∧ 2𝑜 ∈ 𝑗) → {∅} ∈ ∪ 𝑗)
13	11, 12	mpan 702	. . . . . . . . . . . . . . . . . . 19 ⊢ (2𝑜 ∈ 𝑗 → {∅} ∈ ∪ 𝑗)
14		df1o2 7459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1𝑜 = {∅}
15		1on 7454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1𝑜 ∈ On
16	14, 15	eqeltrri 2685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {∅} ∈ On
17	16	onirri 5751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ¬ {∅} ∈ {∅}
18	17	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (2𝑜 ∈ 𝑗 → ¬ {∅} ∈ {∅})
19	13, 18	eldifd 3551	. . . . . . . . . . . . . . . . . 18 ⊢ (2𝑜 ∈ 𝑗 → {∅} ∈ (∪ 𝑗 ∖ {∅}))
20		ne0i 3880	. . . . . . . . . . . . . . . . . 18 ⊢ ({∅} ∈ (∪ 𝑗 ∖ {∅}) → (∪ 𝑗 ∖ {∅}) ≠ ∅)
21	19, 20	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (2𝑜 ∈ 𝑗 → (∪ 𝑗 ∖ {∅}) ≠ ∅)
22	7, 21	2thd 254	. . . . . . . . . . . . . . . 16 ⊢ (2𝑜 ∈ 𝑗 → (¬ ∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
23		nbbn 372	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅) ↔ ¬ (∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
24	22, 23	sylib 207	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 ∈ 𝑗 → ¬ (∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
25		on0eln0 5697	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑗 ∖ {∅}) ∈ On → (∅ ∈ (∪ 𝑗 ∖ {∅}) ↔ (∪ 𝑗 ∖ {∅}) ≠ ∅))
26	24, 25	nsyl 134	. . . . . . . . . . . . . 14 ⊢ (2𝑜 ∈ 𝑗 → ¬ (∪ 𝑗 ∖ {∅}) ∈ On)
27	6, 26	nsyli 154	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ On → (2𝑜 ∈ 𝑗 → ¬ (∪ 𝑗 ∖ {∅}) ∈ 𝑗))
28	27	imp 444	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → ¬ (∪ 𝑗 ∖ {∅}) ∈ 𝑗)
29		0ex 4718	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
30	29	prid1 4241	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅, {∅}}
31	30, 10	eleqtrri 2687	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ 2𝑜
32		elunii 4377	. . . . . . . . . . . . . . . 16 ⊢ ((∅ ∈ 2𝑜 ∧ 2𝑜 ∈ 𝑗) → ∅ ∈ ∪ 𝑗)
33	31, 32	mpan 702	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 ∈ 𝑗 → ∅ ∈ ∪ 𝑗)
34	33	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → ∅ ∈ ∪ 𝑗)
35		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → 𝑎 = ∅)
36	35	sneqd 4137	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → {𝑎} = {∅})
37	36	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) ∧ 𝑎 = ∅) → ({𝑎} ∈ (Clsd‘𝑗) ↔ {∅} ∈ (Clsd‘𝑗)))
38	34, 37	rspcdv 3285	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → {∅} ∈ (Clsd‘𝑗)))
39	2	cldopn 20645	. . . . . . . . . . . . 13 ⊢ ({∅} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗)
40	38, 39	syl6 34	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → (∪ 𝑗 ∖ {∅}) ∈ 𝑗))
41	28, 40	mtod 188	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ 𝑗) → ¬ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗))
42	41	ex 449	. . . . . . . . . 10 ⊢ (𝑗 ∈ On → (2𝑜 ∈ 𝑗 → ¬ ∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗)))
43	42	con2d 128	. . . . . . . . 9 ⊢ (𝑗 ∈ On → (∀𝑎 ∈ ∪ 𝑗{𝑎} ∈ (Clsd‘𝑗) → ¬ 2𝑜 ∈ 𝑗))
44	4, 43	syl5 33	. . . . . . . 8 ⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → ¬ 2𝑜 ∈ 𝑗))
45		2on 7455	. . . . . . . . 9 ⊢ 2𝑜 ∈ On
46		ontri1 5674	. . . . . . . . . 10 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ On) → (𝑗 ⊆ 2𝑜 ↔ ¬ 2𝑜 ∈ 𝑗))
47		onsssuc 5730	. . . . . . . . . 10 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ On) → (𝑗 ⊆ 2𝑜 ↔ 𝑗 ∈ suc 2𝑜))
48	46, 47	bitr3d 269	. . . . . . . . 9 ⊢ ((𝑗 ∈ On ∧ 2𝑜 ∈ On) → (¬ 2𝑜 ∈ 𝑗 ↔ 𝑗 ∈ suc 2𝑜))
49	45, 48	mpan2 703	. . . . . . . 8 ⊢ (𝑗 ∈ On → (¬ 2𝑜 ∈ 𝑗 ↔ 𝑗 ∈ suc 2𝑜))
50	44, 49	sylibd 228	. . . . . . 7 ⊢ (𝑗 ∈ On → (𝑗 ∈ Fre → 𝑗 ∈ suc 2𝑜))
51	50	imp 444	. . . . . 6 ⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ suc 2𝑜)
52		0ntop 20535	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ Top
53		t1top 20944	. . . . . . . . . 10 ⊢ (∅ ∈ Fre → ∅ ∈ Top)
54	52, 53	mto 187	. . . . . . . . 9 ⊢ ¬ ∅ ∈ Fre
55		nelneq 2712	. . . . . . . . 9 ⊢ ((𝑗 ∈ Fre ∧ ¬ ∅ ∈ Fre) → ¬ 𝑗 = ∅)
56	54, 55	mpan2 703	. . . . . . . 8 ⊢ (𝑗 ∈ Fre → ¬ 𝑗 = ∅)
57		elsni 4142	. . . . . . . 8 ⊢ (𝑗 ∈ {∅} → 𝑗 = ∅)
58	56, 57	nsyl 134	. . . . . . 7 ⊢ (𝑗 ∈ Fre → ¬ 𝑗 ∈ {∅})
59	58	adantl 481	. . . . . 6 ⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → ¬ 𝑗 ∈ {∅})
60	51, 59	eldifd 3551	. . . . 5 ⊢ ((𝑗 ∈ On ∧ 𝑗 ∈ Fre) → 𝑗 ∈ (suc 2𝑜 ∖ {∅}))
61	1, 60	sylbi 206	. . . 4 ⊢ (𝑗 ∈ (On ∩ Fre) → 𝑗 ∈ (suc 2𝑜 ∖ {∅}))
62	61	ssriv 3572	. . 3 ⊢ (On ∩ Fre) ⊆ (suc 2𝑜 ∖ {∅})
63		df-suc 5646	. . . . . 6 ⊢ suc 2𝑜 = (2𝑜 ∪ {2𝑜})
64	63	difeq1i 3686	. . . . 5 ⊢ (suc 2𝑜 ∖ {∅}) = ((2𝑜 ∪ {2𝑜}) ∖ {∅})
65		difundir 3839	. . . . 5 ⊢ ((2𝑜 ∪ {2𝑜}) ∖ {∅}) = ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅}))
66	64, 65	eqtri 2632	. . . 4 ⊢ (suc 2𝑜 ∖ {∅}) = ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅}))
67		df-pr 4128	. . . . 5 ⊢ {1𝑜, 2𝑜} = ({1𝑜} ∪ {2𝑜})
68		df2o3 7460	. . . . . . . . 9 ⊢ 2𝑜 = {∅, 1𝑜}
69		df-pr 4128	. . . . . . . . 9 ⊢ {∅, 1𝑜} = ({∅} ∪ {1𝑜})
70	68, 69	eqtri 2632	. . . . . . . 8 ⊢ 2𝑜 = ({∅} ∪ {1𝑜})
71	70	difeq1i 3686	. . . . . . 7 ⊢ (2𝑜 ∖ {∅}) = (({∅} ∪ {1𝑜}) ∖ {∅})
72		difundir 3839	. . . . . . 7 ⊢ (({∅} ∪ {1𝑜}) ∖ {∅}) = (({∅} ∖ {∅}) ∪ ({1𝑜} ∖ {∅}))
73		difid 3902	. . . . . . . . 9 ⊢ ({∅} ∖ {∅}) = ∅
74		1n0 7462	. . . . . . . . . . . 12 ⊢ 1𝑜 ≠ ∅
75		disjsn2 4193	. . . . . . . . . . . 12 ⊢ (1𝑜 ≠ ∅ → ({1𝑜} ∩ {∅}) = ∅)
76	74, 75	ax-mp 5	. . . . . . . . . . 11 ⊢ ({1𝑜} ∩ {∅}) = ∅
77	76	difeq2i 3687	. . . . . . . . . 10 ⊢ ({1𝑜} ∖ ({1𝑜} ∩ {∅})) = ({1𝑜} ∖ ∅)
78		difin 3823	. . . . . . . . . 10 ⊢ ({1𝑜} ∖ ({1𝑜} ∩ {∅})) = ({1𝑜} ∖ {∅})
79		dif0 3904	. . . . . . . . . 10 ⊢ ({1𝑜} ∖ ∅) = {1𝑜}
80	77, 78, 79	3eqtr3i 2640	. . . . . . . . 9 ⊢ ({1𝑜} ∖ {∅}) = {1𝑜}
81	73, 80	uneq12i 3727	. . . . . . . 8 ⊢ (({∅} ∖ {∅}) ∪ ({1𝑜} ∖ {∅})) = (∅ ∪ {1𝑜})
82		uncom 3719	. . . . . . . 8 ⊢ (∅ ∪ {1𝑜}) = ({1𝑜} ∪ ∅)
83		un0 3919	. . . . . . . 8 ⊢ ({1𝑜} ∪ ∅) = {1𝑜}
84	81, 82, 83	3eqtri 2636	. . . . . . 7 ⊢ (({∅} ∖ {∅}) ∪ ({1𝑜} ∖ {∅})) = {1𝑜}
85	71, 72, 84	3eqtri 2636	. . . . . 6 ⊢ (2𝑜 ∖ {∅}) = {1𝑜}
86		2on0 7456	. . . . . . . . 9 ⊢ 2𝑜 ≠ ∅
87		disjsn2 4193	. . . . . . . . 9 ⊢ (2𝑜 ≠ ∅ → ({2𝑜} ∩ {∅}) = ∅)
88	86, 87	ax-mp 5	. . . . . . . 8 ⊢ ({2𝑜} ∩ {∅}) = ∅
89	88	difeq2i 3687	. . . . . . 7 ⊢ ({2𝑜} ∖ ({2𝑜} ∩ {∅})) = ({2𝑜} ∖ ∅)
90		difin 3823	. . . . . . 7 ⊢ ({2𝑜} ∖ ({2𝑜} ∩ {∅})) = ({2𝑜} ∖ {∅})
91		dif0 3904	. . . . . . 7 ⊢ ({2𝑜} ∖ ∅) = {2𝑜}
92	89, 90, 91	3eqtr3i 2640	. . . . . 6 ⊢ ({2𝑜} ∖ {∅}) = {2𝑜}
93	85, 92	uneq12i 3727	. . . . 5 ⊢ ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅})) = ({1𝑜} ∪ {2𝑜})
94	67, 93	eqtr4i 2635	. . . 4 ⊢ {1𝑜, 2𝑜} = ((2𝑜 ∖ {∅}) ∪ ({2𝑜} ∖ {∅}))
95	66, 94	eqtr4i 2635	. . 3 ⊢ (suc 2𝑜 ∖ {∅}) = {1𝑜, 2𝑜}
96	62, 95	sseqtri 3600	. 2 ⊢ (On ∩ Fre) ⊆ {1𝑜, 2𝑜}
97		ssoninhaus 31617	. . 3 ⊢ {1𝑜, 2𝑜} ⊆ (On ∩ Haus)
98		haust1 20966	. . . . 5 ⊢ (𝑗 ∈ Haus → 𝑗 ∈ Fre)
99	98	ssriv 3572	. . . 4 ⊢ Haus ⊆ Fre
100		sslin 3801	. . . 4 ⊢ (Haus ⊆ Fre → (On ∩ Haus) ⊆ (On ∩ Fre))
101	99, 100	ax-mp 5	. . 3 ⊢ (On ∩ Haus) ⊆ (On ∩ Fre)
102	97, 101	sstri 3577	. 2 ⊢ {1𝑜, 2𝑜} ⊆ (On ∩ Fre)
103	96, 102	eqssi 3584	1 ⊢ (On ∩ Fre) = {1𝑜, 2𝑜}

Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  {cpr 4127  ∪ cuni 4372  Oncon0 5640  suc csuc 5642  ‘cfv 5804  1_𝑜c1o 7440  2_𝑜c2o 7441  Topctop 20517  Clsdccld 20630  Frect1 20921  Hauscha 20922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-ord 5643  df-on 5644  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-1o 7447  df-2o 7448  df-topgen 15927  df-top 20521  df-topon 20523  df-cld 20633  df-t1 20928  df-haus 20929

This theorem is referenced by:  oninhaus  31619