Metamath Proof Explorer

Theorem alephordi

Description: Strict ordering property of the aleph function. (Contributed by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephordi 
|- ( B e. On -> ( A e. B -> ( aleph ` A ) ~< ( aleph ` B ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = (/) -> ( A e. x <-> A e. (/) ) )
2 fveq2 
 |-  ( x = (/) -> ( aleph ` x ) = ( aleph ` (/) ) )
3 2 breq2d 
 |-  ( x = (/) -> ( ( aleph ` A ) ~< ( aleph ` x ) <-> ( aleph ` A ) ~< ( aleph ` (/) ) ) )
4 1 3 imbi12d 
 |-  ( x = (/) -> ( ( A e. x -> ( aleph ` A ) ~< ( aleph ` x ) ) <-> ( A e. (/) -> ( aleph ` A ) ~< ( aleph ` (/) ) ) ) )
5 eleq2 
 |-  ( x = y -> ( A e. x <-> A e. y ) )
6 fveq2 
 |-  ( x = y -> ( aleph ` x ) = ( aleph ` y ) )
7 6 breq2d 
 |-  ( x = y -> ( ( aleph ` A ) ~< ( aleph ` x ) <-> ( aleph ` A ) ~< ( aleph ` y ) ) )
8 5 7 imbi12d 
 |-  ( x = y -> ( ( A e. x -> ( aleph ` A ) ~< ( aleph ` x ) ) <-> ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) ) )
9 eleq2 
 |-  ( x = suc y -> ( A e. x <-> A e. suc y ) )
10 fveq2 
 |-  ( x = suc y -> ( aleph ` x ) = ( aleph ` suc y ) )
11 10 breq2d 
 |-  ( x = suc y -> ( ( aleph ` A ) ~< ( aleph ` x ) <-> ( aleph ` A ) ~< ( aleph ` suc y ) ) )
12 9 11 imbi12d 
 |-  ( x = suc y -> ( ( A e. x -> ( aleph ` A ) ~< ( aleph ` x ) ) <-> ( A e. suc y -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
13 eleq2 
 |-  ( x = B -> ( A e. x <-> A e. B ) )
14 fveq2 
 |-  ( x = B -> ( aleph ` x ) = ( aleph ` B ) )
15 14 breq2d 
 |-  ( x = B -> ( ( aleph ` A ) ~< ( aleph ` x ) <-> ( aleph ` A ) ~< ( aleph ` B ) ) )
16 13 15 imbi12d 
 |-  ( x = B -> ( ( A e. x -> ( aleph ` A ) ~< ( aleph ` x ) ) <-> ( A e. B -> ( aleph ` A ) ~< ( aleph ` B ) ) ) )
17 noel 
 |-  -. A e. (/)
18 17 pm2.21i 
 |-  ( A e. (/) -> ( aleph ` A ) ~< ( aleph ` (/) ) )
19 vex 
 |-  y e. _V
20 19 elsuc2 
 |-  ( A e. suc y <-> ( A e. y \/ A = y ) )
21 alephordilem1 
 |-  ( y e. On -> ( aleph ` y ) ~< ( aleph ` suc y ) )
22 sdomtr 
 |-  ( ( ( aleph ` A ) ~< ( aleph ` y ) /\ ( aleph ` y ) ~< ( aleph ` suc y ) ) -> ( aleph ` A ) ~< ( aleph ` suc y ) )
23 21 22 sylan2 
 |-  ( ( ( aleph ` A ) ~< ( aleph ` y ) /\ y e. On ) -> ( aleph ` A ) ~< ( aleph ` suc y ) )
24 23 expcom 
 |-  ( y e. On -> ( ( aleph ` A ) ~< ( aleph ` y ) -> ( aleph ` A ) ~< ( aleph ` suc y ) ) )
25 24 imim2d 
 |-  ( y e. On -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( A e. y -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
26 25 com23 
 |-  ( y e. On -> ( A e. y -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
27 fveq2 
 |-  ( A = y -> ( aleph ` A ) = ( aleph ` y ) )
28 27 breq1d 
 |-  ( A = y -> ( ( aleph ` A ) ~< ( aleph ` suc y ) <-> ( aleph ` y ) ~< ( aleph ` suc y ) ) )
29 21 28 syl5ibr 
 |-  ( A = y -> ( y e. On -> ( aleph ` A ) ~< ( aleph ` suc y ) ) )
30 29 a1d 
 |-  ( A = y -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( y e. On -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
31 30 com3r 
 |-  ( y e. On -> ( A = y -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
32 26 31 jaod 
 |-  ( y e. On -> ( ( A e. y \/ A = y ) -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
33 20 32 syl5bi 
 |-  ( y e. On -> ( A e. suc y -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
34 33 com23 
 |-  ( y e. On -> ( ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( A e. suc y -> ( aleph ` A ) ~< ( aleph ` suc y ) ) ) )
35 fvexd 
 |-  ( Lim x -> ( aleph ` x ) e. _V )
36 fveq2 
 |-  ( w = A -> ( aleph ` w ) = ( aleph ` A ) )
37 36 ssiun2s 
 |-  ( A e. x -> ( aleph ` A ) C_ U_ w e. x ( aleph ` w ) )
38 vex 
 |-  x e. _V
39 alephlim 
 |-  ( ( x e. _V /\ Lim x ) -> ( aleph ` x ) = U_ w e. x ( aleph ` w ) )
40 38 39 mpan 
 |-  ( Lim x -> ( aleph ` x ) = U_ w e. x ( aleph ` w ) )
41 40 sseq2d 
 |-  ( Lim x -> ( ( aleph ` A ) C_ ( aleph ` x ) <-> ( aleph ` A ) C_ U_ w e. x ( aleph ` w ) ) )
42 37 41 syl5ibr 
 |-  ( Lim x -> ( A e. x -> ( aleph ` A ) C_ ( aleph ` x ) ) )
43 ssdomg 
 |-  ( ( aleph ` x ) e. _V -> ( ( aleph ` A ) C_ ( aleph ` x ) -> ( aleph ` A ) ~<_ ( aleph ` x ) ) )
44 35 42 43 sylsyld 
 |-  ( Lim x -> ( A e. x -> ( aleph ` A ) ~<_ ( aleph ` x ) ) )
45 limsuc 
 |-  ( Lim x -> ( A e. x <-> suc A e. x ) )
46 fveq2 
 |-  ( w = suc A -> ( aleph ` w ) = ( aleph ` suc A ) )
47 46 ssiun2s 
 |-  ( suc A e. x -> ( aleph ` suc A ) C_ U_ w e. x ( aleph ` w ) )
48 40 sseq2d 
 |-  ( Lim x -> ( ( aleph ` suc A ) C_ ( aleph ` x ) <-> ( aleph ` suc A ) C_ U_ w e. x ( aleph ` w ) ) )
49 47 48 syl5ibr 
 |-  ( Lim x -> ( suc A e. x -> ( aleph ` suc A ) C_ ( aleph ` x ) ) )
50 ssdomg 
 |-  ( ( aleph ` x ) e. _V -> ( ( aleph ` suc A ) C_ ( aleph ` x ) -> ( aleph ` suc A ) ~<_ ( aleph ` x ) ) )
51 35 49 50 sylsyld 
 |-  ( Lim x -> ( suc A e. x -> ( aleph ` suc A ) ~<_ ( aleph ` x ) ) )
52 45 51 sylbid 
 |-  ( Lim x -> ( A e. x -> ( aleph ` suc A ) ~<_ ( aleph ` x ) ) )
53 52 imp 
 |-  ( ( Lim x /\ A e. x ) -> ( aleph ` suc A ) ~<_ ( aleph ` x ) )
54 domnsym 
 |-  ( ( aleph ` suc A ) ~<_ ( aleph ` x ) -> -. ( aleph ` x ) ~< ( aleph ` suc A ) )
55 53 54 syl 
 |-  ( ( Lim x /\ A e. x ) -> -. ( aleph ` x ) ~< ( aleph ` suc A ) )
56 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
57 38 56 mpan 
 |-  ( Lim x -> x e. On )
58 onelon 
 |-  ( ( x e. On /\ A e. x ) -> A e. On )
59 57 58 sylan 
 |-  ( ( Lim x /\ A e. x ) -> A e. On )
60 ensym 
 |-  ( ( aleph ` A ) ~~ ( aleph ` x ) -> ( aleph ` x ) ~~ ( aleph ` A ) )
61 alephordilem1 
 |-  ( A e. On -> ( aleph ` A ) ~< ( aleph ` suc A ) )
62 ensdomtr 
 |-  ( ( ( aleph ` x ) ~~ ( aleph ` A ) /\ ( aleph ` A ) ~< ( aleph ` suc A ) ) -> ( aleph ` x ) ~< ( aleph ` suc A ) )
63 62 ex 
 |-  ( ( aleph ` x ) ~~ ( aleph ` A ) -> ( ( aleph ` A ) ~< ( aleph ` suc A ) -> ( aleph ` x ) ~< ( aleph ` suc A ) ) )
64 60 61 63 syl2im 
 |-  ( ( aleph ` A ) ~~ ( aleph ` x ) -> ( A e. On -> ( aleph ` x ) ~< ( aleph ` suc A ) ) )
65 59 64 syl5com 
 |-  ( ( Lim x /\ A e. x ) -> ( ( aleph ` A ) ~~ ( aleph ` x ) -> ( aleph ` x ) ~< ( aleph ` suc A ) ) )
66 55 65 mtod 
 |-  ( ( Lim x /\ A e. x ) -> -. ( aleph ` A ) ~~ ( aleph ` x ) )
67 66 ex 
 |-  ( Lim x -> ( A e. x -> -. ( aleph ` A ) ~~ ( aleph ` x ) ) )
68 44 67 jcad 
 |-  ( Lim x -> ( A e. x -> ( ( aleph ` A ) ~<_ ( aleph ` x ) /\ -. ( aleph ` A ) ~~ ( aleph ` x ) ) ) )
69 brsdom 
 |-  ( ( aleph ` A ) ~< ( aleph ` x ) <-> ( ( aleph ` A ) ~<_ ( aleph ` x ) /\ -. ( aleph ` A ) ~~ ( aleph ` x ) ) )
70 68 69 syl6ibr 
 |-  ( Lim x -> ( A e. x -> ( aleph ` A ) ~< ( aleph ` x ) ) )
71 70 a1d 
 |-  ( Lim x -> ( A. y e. x ( A e. y -> ( aleph ` A ) ~< ( aleph ` y ) ) -> ( A e. x -> ( aleph ` A ) ~< ( aleph ` x ) ) ) )
72 4 8 12 16 18 34 71 tfinds 
 |-  ( B e. On -> ( A e. B -> ( aleph ` A ) ~< ( aleph ` B ) ) )