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 e. On -> suc A e. Kol2 )

Proof

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