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