Metamath Proof Explorer

Theorem winainflem

Description: A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014)

Ref Expression
Assertion winainflem 
|- ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> _om C_ A )

Proof

Step Hyp Ref Expression
1 nn0suc 
 |-  ( A e. _om -> ( A = (/) \/ E. z e. _om A = suc z ) )
2 simp1 
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> A =/= (/) )
3 2 necon2bi 
 |-  ( A = (/) -> -. ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) )
4 vex 
 |-  z e. _V
5 4 sucid 
 |-  z e. suc z
6 eleq2 
 |-  ( A = suc z -> ( z e. A <-> z e. suc z ) )
7 5 6 mpbiri 
 |-  ( A = suc z -> z e. A )
8 7 adantl 
 |-  ( ( z e. _om /\ A = suc z ) -> z e. A )
9 breq1 
 |-  ( x = z -> ( x ~< y <-> z ~< y ) )
10 9 rexbidv 
 |-  ( x = z -> ( E. y e. A x ~< y <-> E. y e. A z ~< y ) )
11 breq2 
 |-  ( y = w -> ( z ~< y <-> z ~< w ) )
12 11 cbvrexvw 
 |-  ( E. y e. A z ~< y <-> E. w e. A z ~< w )
13 10 12 bitrdi 
 |-  ( x = z -> ( E. y e. A x ~< y <-> E. w e. A z ~< w ) )
14 13 rspcv 
 |-  ( z e. A -> ( A. x e. A E. y e. A x ~< y -> E. w e. A z ~< w ) )
15 8 14 syl 
 |-  ( ( z e. _om /\ A = suc z ) -> ( A. x e. A E. y e. A x ~< y -> E. w e. A z ~< w ) )
16 eleq2 
 |-  ( A = suc z -> ( w e. A <-> w e. suc z ) )
17 16 biimpa 
 |-  ( ( A = suc z /\ w e. A ) -> w e. suc z )
18 17 3ad2antl2 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> w e. suc z )
19 nnon 
 |-  ( z e. _om -> z e. On )
20 suceloni 
 |-  ( z e. On -> suc z e. On )
21 19 20 syl 
 |-  ( z e. _om -> suc z e. On )
22 eleq1 
 |-  ( A = suc z -> ( A e. On <-> suc z e. On ) )
23 22 biimparc 
 |-  ( ( suc z e. On /\ A = suc z ) -> A e. On )
24 21 23 sylan 
 |-  ( ( z e. _om /\ A = suc z ) -> A e. On )
25 24 3adant3 
 |-  ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) -> A e. On )
26 onelon 
 |-  ( ( A e. On /\ w e. A ) -> w e. On )
27 25 26 sylan 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> w e. On )
28 simpl1 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> z e. _om )
29 28 19 syl 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> z e. On )
30 onsssuc 
 |-  ( ( w e. On /\ z e. On ) -> ( w C_ z <-> w e. suc z ) )
31 27 29 30 syl2anc 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> ( w C_ z <-> w e. suc z ) )
32 18 31 mpbird 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> w C_ z )
33 ssdomg 
 |-  ( z e. _V -> ( w C_ z -> w ~<_ z ) )
34 4 32 33 mpsyl 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> w ~<_ z )
35 domnsym 
 |-  ( w ~<_ z -> -. z ~< w )
36 34 35 syl 
 |-  ( ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) /\ w e. A ) -> -. z ~< w )
37 36 nrexdv 
 |-  ( ( z e. _om /\ A = suc z /\ A. x e. A E. y e. A x ~< y ) -> -. E. w e. A z ~< w )
38 37 3expia 
 |-  ( ( z e. _om /\ A = suc z ) -> ( A. x e. A E. y e. A x ~< y -> -. E. w e. A z ~< w ) )
39 15 38 pm2.65d 
 |-  ( ( z e. _om /\ A = suc z ) -> -. A. x e. A E. y e. A x ~< y )
40 39 intn3an3d 
 |-  ( ( z e. _om /\ A = suc z ) -> -. ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) )
41 40 rexlimiva 
 |-  ( E. z e. _om A = suc z -> -. ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) )
42 3 41 jaoi 
 |-  ( ( A = (/) \/ E. z e. _om A = suc z ) -> -. ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) )
43 1 42 syl 
 |-  ( A e. _om -> -. ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) )
44 43 con2i 
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> -. A e. _om )
45 ordom 
 |-  Ord _om
46 eloni 
 |-  ( A e. On -> Ord A )
47 46 3ad2ant2 
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> Ord A )
48 ordtri1 
 |-  ( ( Ord _om /\ Ord A ) -> ( _om C_ A <-> -. A e. _om ) )
49 45 47 48 sylancr 
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> ( _om C_ A <-> -. A e. _om ) )
50 44 49 mpbird 
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> _om C_ A )