Metamath Proof Explorer

Theorem onsuct0

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

Ref Expression
Assertion onsuct0 ⊢ A ∈ On → suc ⁡ A ∈ Kol2

Proof

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