Metamath Proof Explorer

Theorem r1sdom

Description: Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013)

Ref Expression
Assertion r1sdom 
|- ( ( A e. On /\ B e. A ) -> ( R1 ` B ) ~< ( R1 ` A ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = (/) -> ( B e. x <-> B e. (/) ) )
2 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
3 2 breq2d 
 |-  ( x = (/) -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` (/) ) ) )
4 1 3 imbi12d 
 |-  ( x = (/) -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. (/) -> ( R1 ` B ) ~< ( R1 ` (/) ) ) ) )
5 eleq2 
 |-  ( x = y -> ( B e. x <-> B e. y ) )
6 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
7 6 breq2d 
 |-  ( x = y -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` y ) ) )
8 5 7 imbi12d 
 |-  ( x = y -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) ) )
9 eleq2 
 |-  ( x = suc y -> ( B e. x <-> B e. suc y ) )
10 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
11 10 breq2d 
 |-  ( x = suc y -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
12 9 11 imbi12d 
 |-  ( x = suc y -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. suc y -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
13 eleq2 
 |-  ( x = A -> ( B e. x <-> B e. A ) )
14 fveq2 
 |-  ( x = A -> ( R1 ` x ) = ( R1 ` A ) )
15 14 breq2d 
 |-  ( x = A -> ( ( R1 ` B ) ~< ( R1 ` x ) <-> ( R1 ` B ) ~< ( R1 ` A ) ) )
16 13 15 imbi12d 
 |-  ( x = A -> ( ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) <-> ( B e. A -> ( R1 ` B ) ~< ( R1 ` A ) ) ) )
17 noel 
 |-  -. B e. (/)
18 17 pm2.21i 
 |-  ( B e. (/) -> ( R1 ` B ) ~< ( R1 ` (/) ) )
19 elsuci 
 |-  ( B e. suc y -> ( B e. y \/ B = y ) )
20 sdomtr 
 |-  ( ( ( R1 ` B ) ~< ( R1 ` y ) /\ ( R1 ` y ) ~< ( R1 ` suc y ) ) -> ( R1 ` B ) ~< ( R1 ` suc y ) )
21 20 expcom 
 |-  ( ( R1 ` y ) ~< ( R1 ` suc y ) -> ( ( R1 ` B ) ~< ( R1 ` y ) -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
22 fvex 
 |-  ( R1 ` y ) e. _V
23 22 canth2 
 |-  ( R1 ` y ) ~< ~P ( R1 ` y )
24 r1suc 
 |-  ( y e. On -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
25 23 24 breqtrrid 
 |-  ( y e. On -> ( R1 ` y ) ~< ( R1 ` suc y ) )
26 21 25 syl11 
 |-  ( ( R1 ` B ) ~< ( R1 ` y ) -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
27 26 imim2i 
 |-  ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
28 fveq2 
 |-  ( B = y -> ( R1 ` B ) = ( R1 ` y ) )
29 28 breq1d 
 |-  ( B = y -> ( ( R1 ` B ) ~< ( R1 ` suc y ) <-> ( R1 ` y ) ~< ( R1 ` suc y ) ) )
30 25 29 syl5ibr 
 |-  ( B = y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) )
31 30 a1i 
 |-  ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B = y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
32 27 31 jaod 
 |-  ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( ( B e. y \/ B = y ) -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
33 19 32 syl5 
 |-  ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. suc y -> ( y e. On -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
34 33 com3r 
 |-  ( y e. On -> ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. suc y -> ( R1 ` B ) ~< ( R1 ` suc y ) ) ) )
35 limuni 
 |-  ( Lim x -> x = U. x )
36 35 eleq2d 
 |-  ( Lim x -> ( B e. x <-> B e. U. x ) )
37 eluni2 
 |-  ( B e. U. x <-> E. y e. x B e. y )
38 36 37 bitrdi 
 |-  ( Lim x -> ( B e. x <-> E. y e. x B e. y ) )
39 r19.29 
 |-  ( ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ E. y e. x B e. y ) -> E. y e. x ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) )
40 fvex 
 |-  ( R1 ` x ) e. _V
41 ssiun2 
 |-  ( y e. x -> ( R1 ` y ) C_ U_ y e. x ( R1 ` y ) )
42 vex 
 |-  x e. _V
43 r1lim 
 |-  ( ( x e. _V /\ Lim x ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
44 42 43 mpan 
 |-  ( Lim x -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
45 44 sseq2d 
 |-  ( Lim x -> ( ( R1 ` y ) C_ ( R1 ` x ) <-> ( R1 ` y ) C_ U_ y e. x ( R1 ` y ) ) )
46 41 45 syl5ibr 
 |-  ( Lim x -> ( y e. x -> ( R1 ` y ) C_ ( R1 ` x ) ) )
47 ssdomg 
 |-  ( ( R1 ` x ) e. _V -> ( ( R1 ` y ) C_ ( R1 ` x ) -> ( R1 ` y ) ~<_ ( R1 ` x ) ) )
48 40 46 47 mpsylsyld 
 |-  ( Lim x -> ( y e. x -> ( R1 ` y ) ~<_ ( R1 ` x ) ) )
49 id 
 |-  ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) )
50 49 imp 
 |-  ( ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` y ) )
51 sdomdomtr 
 |-  ( ( ( R1 ` B ) ~< ( R1 ` y ) /\ ( R1 ` y ) ~<_ ( R1 ` x ) ) -> ( R1 ` B ) ~< ( R1 ` x ) )
52 51 expcom 
 |-  ( ( R1 ` y ) ~<_ ( R1 ` x ) -> ( ( R1 ` B ) ~< ( R1 ` y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
53 50 52 syl5 
 |-  ( ( R1 ` y ) ~<_ ( R1 ` x ) -> ( ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
54 48 53 syl6 
 |-  ( Lim x -> ( y e. x -> ( ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
55 54 rexlimdv 
 |-  ( Lim x -> ( E. y e. x ( ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
56 39 55 syl5 
 |-  ( Lim x -> ( ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) /\ E. y e. x B e. y ) -> ( R1 ` B ) ~< ( R1 ` x ) ) )
57 56 expcomd 
 |-  ( Lim x -> ( E. y e. x B e. y -> ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
58 38 57 sylbid 
 |-  ( Lim x -> ( B e. x -> ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
59 58 com23 
 |-  ( Lim x -> ( A. y e. x ( B e. y -> ( R1 ` B ) ~< ( R1 ` y ) ) -> ( B e. x -> ( R1 ` B ) ~< ( R1 ` x ) ) ) )
60 4 8 12 16 18 34 59 tfinds 
 |-  ( A e. On -> ( B e. A -> ( R1 ` B ) ~< ( R1 ` A ) ) )
61 60 imp 
 |-  ( ( A e. On /\ B e. A ) -> ( R1 ` B ) ~< ( R1 ` A ) )