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 \cap Fre = \{1_{𝑜}, 2_{𝑜}\}$

Proof

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

Metamath Proof Explorer

Theorem onint1

Proof