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 ) )