onsuct0

Description: A successor ordinal number is a T_0 space. (Contributed by Chen-Pang He, 8-Nov-2015)

		Ref	Expression
	Assertion	onsuct0	$⊢ A \in On \to suc A \in Kol2$

Proof

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		df-ral	$⊢ \forall o \in suc A (x \in o \leftrightarrow y \in o) \leftrightarrow \forall o (o \in suc A \to (x \in o \leftrightarrow y \in o))$
3		ordelon	$⊢ (Ord A \land x \in A) \to x \in On$
4		ordelon	$⊢ (Ord A \land y \in A) \to y \in On$
5	3 4	anim12dan	$⊢ (Ord A \land (x \in A \land y \in A)) \to (x \in On \land y \in On)$
6		ordsuc	$⊢ Ord A \leftrightarrow Ord suc A$
7		ordelon	$⊢ (Ord suc A \land o \in suc A) \to o \in On$
8	7	ex	$⊢ Ord suc A \to (o \in suc A \to o \in On)$
9	6 8	sylbi	$⊢ Ord A \to (o \in suc A \to o \in On)$
10	9	adantr	$⊢ (Ord A \land (x \in A \land y \in A)) \to (o \in suc A \to o \in On)$
11		notbi	$⊢ (x \in o \leftrightarrow y \in o) \leftrightarrow (\neg x \in o \leftrightarrow \neg y \in o)$
12		ontri1	$⊢ (o \in On \land x \in On) \to (o \subseteq x \leftrightarrow \neg x \in o)$
13		onsssuc	$⊢ (o \in On \land x \in On) \to (o \subseteq x \leftrightarrow o \in suc x)$
14	12 13	bitr3d	$⊢ (o \in On \land x \in On) \to (\neg x \in o \leftrightarrow o \in suc x)$
15	14	adantrr	$⊢ (o \in On \land (x \in On \land y \in On)) \to (\neg x \in o \leftrightarrow o \in suc x)$
16		ontri1	$⊢ (o \in On \land y \in On) \to (o \subseteq y \leftrightarrow \neg y \in o)$
17		onsssuc	$⊢ (o \in On \land y \in On) \to (o \subseteq y \leftrightarrow o \in suc y)$
18	16 17	bitr3d	$⊢ (o \in On \land y \in On) \to (\neg y \in o \leftrightarrow o \in suc y)$
19	18	adantrl	$⊢ (o \in On \land (x \in On \land y \in On)) \to (\neg y \in o \leftrightarrow o \in suc y)$
20	15 19	bibi12d	$⊢ (o \in On \land (x \in On \land y \in On)) \to ((\neg x \in o \leftrightarrow \neg y \in o) \leftrightarrow (o \in suc x \leftrightarrow o \in suc y))$
21	20	ancoms	$⊢ ((x \in On \land y \in On) \land o \in On) \to ((\neg x \in o \leftrightarrow \neg y \in o) \leftrightarrow (o \in suc x \leftrightarrow o \in suc y))$
22	11 21	bitrid	$⊢ ((x \in On \land y \in On) \land o \in On) \to ((x \in o \leftrightarrow y \in o) \leftrightarrow (o \in suc x \leftrightarrow o \in suc y))$
23	22	biimpd	$⊢ ((x \in On \land y \in On) \land o \in On) \to ((x \in o \leftrightarrow y \in o) \to (o \in suc x \leftrightarrow o \in suc y))$
24	5 10 23	syl6an	$⊢ (Ord A \land (x \in A \land y \in A)) \to (o \in suc A \to ((x \in o \leftrightarrow y \in o) \to (o \in suc x \leftrightarrow o \in suc y)))$
25	24	a2d	$⊢ (Ord A \land (x \in A \land y \in A)) \to ((o \in suc A \to (x \in o \leftrightarrow y \in o)) \to (o \in suc A \to (o \in suc x \leftrightarrow o \in suc y)))$
26		ordelss	$⊢ (Ord A \land x \in A) \to x \subseteq A$
27		ordelord	$⊢ (Ord A \land x \in A) \to Ord x$
28		ordsucsssuc	$⊢ (Ord x \land Ord A) \to (x \subseteq A \leftrightarrow suc x \subseteq suc A)$
29	28	ancoms	$⊢ (Ord A \land Ord x) \to (x \subseteq A \leftrightarrow suc x \subseteq suc A)$
30	27 29	syldan	$⊢ (Ord A \land x \in A) \to (x \subseteq A \leftrightarrow suc x \subseteq suc A)$
31	26 30	mpbid	$⊢ (Ord A \land x \in A) \to suc x \subseteq suc A$
32	31	ssneld	$⊢ (Ord A \land x \in A) \to (\neg o \in suc A \to \neg o \in suc x)$
33	32	adantrr	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\neg o \in suc A \to \neg o \in suc x)$
34		ordelss	$⊢ (Ord A \land y \in A) \to y \subseteq A$
35		ordelord	$⊢ (Ord A \land y \in A) \to Ord y$
36		ordsucsssuc	$⊢ (Ord y \land Ord A) \to (y \subseteq A \leftrightarrow suc y \subseteq suc A)$
37	36	ancoms	$⊢ (Ord A \land Ord y) \to (y \subseteq A \leftrightarrow suc y \subseteq suc A)$
38	35 37	syldan	$⊢ (Ord A \land y \in A) \to (y \subseteq A \leftrightarrow suc y \subseteq suc A)$
39	34 38	mpbid	$⊢ (Ord A \land y \in A) \to suc y \subseteq suc A$
40	39	ssneld	$⊢ (Ord A \land y \in A) \to (\neg o \in suc A \to \neg o \in suc y)$
41	40	adantrl	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\neg o \in suc A \to \neg o \in suc y)$
42	33 41	jcad	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\neg o \in suc A \to (\neg o \in suc x \land \neg o \in suc y))$
43		pm5.21	$⊢ (\neg o \in suc x \land \neg o \in suc y) \to (o \in suc x \leftrightarrow o \in suc y)$
44	42 43	syl6	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\neg o \in suc A \to (o \in suc x \leftrightarrow o \in suc y))$
45		idd	$⊢ (Ord A \land (x \in A \land y \in A)) \to ((o \in suc x \leftrightarrow o \in suc y) \to (o \in suc x \leftrightarrow o \in suc y))$
46	44 45	jad	$⊢ (Ord A \land (x \in A \land y \in A)) \to ((o \in suc A \to (o \in suc x \leftrightarrow o \in suc y)) \to (o \in suc x \leftrightarrow o \in suc y))$
47	25 46	syld	$⊢ (Ord A \land (x \in A \land y \in A)) \to ((o \in suc A \to (x \in o \leftrightarrow y \in o)) \to (o \in suc x \leftrightarrow o \in suc y))$
48	47	alimdv	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\forall o (o \in suc A \to (x \in o \leftrightarrow y \in o)) \to \forall o (o \in suc x \leftrightarrow o \in suc y))$
49	2 48	biimtrid	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\forall o \in suc A (x \in o \leftrightarrow y \in o) \to \forall o (o \in suc x \leftrightarrow o \in suc y))$
50		dfcleq	$⊢ suc x = suc y \leftrightarrow \forall o (o \in suc x \leftrightarrow o \in suc y)$
51		suc11	$⊢ (x \in On \land y \in On) \to (suc x = suc y \leftrightarrow x = y)$
52	50 51	bitr3id	$⊢ (x \in On \land y \in On) \to (\forall o (o \in suc x \leftrightarrow o \in suc y) \leftrightarrow x = y)$
53	5 52	syl	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\forall o (o \in suc x \leftrightarrow o \in suc y) \leftrightarrow x = y)$
54	49 53	sylibd	$⊢ (Ord A \land (x \in A \land y \in A)) \to (\forall o \in suc A (x \in o \leftrightarrow y \in o) \to x = y)$
55	54	ralrimivva	$⊢ Ord A \to \forall x \in A \forall y \in A (\forall o \in suc A (x \in o \leftrightarrow y \in o) \to x = y)$
56	1 55	syl	$⊢ A \in On \to \forall x \in A \forall y \in A (\forall o \in suc A (x \in o \leftrightarrow y \in o) \to x = y)$
57		onsuctopon	$⊢ A \in On \to suc A \in TopOn (A)$
58		ist0-2	$⊢ suc A \in TopOn (A) \to (suc A \in Kol2 \leftrightarrow \forall x \in A \forall y \in A (\forall o \in suc A (x \in o \leftrightarrow y \in o) \to x = y))$
59	57 58	syl	$⊢ A \in On \to (suc A \in Kol2 \leftrightarrow \forall x \in A \forall y \in A (\forall o \in suc A (x \in o \leftrightarrow y \in o) \to x = y))$
60	56 59	mpbird	$⊢ A \in On \to suc A \in Kol2$

Metamath Proof Explorer

Theorem onsuct0

Proof