Step |
Hyp |
Ref |
Expression |
1 |
|
rankr1b.1 |
|- A e. _V |
2 |
|
nfcv |
|- F/_ x A |
3 |
|
nfcv |
|- F/_ x R1 |
4 |
|
nfiu1 |
|- F/_ x U_ x e. A suc ( rank ` x ) |
5 |
3 4
|
nffv |
|- F/_ x ( R1 ` U_ x e. A suc ( rank ` x ) ) |
6 |
2 5
|
dfss2f |
|- ( A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) <-> A. x ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) ) |
7 |
|
vex |
|- x e. _V |
8 |
7
|
rankid |
|- x e. ( R1 ` suc ( rank ` x ) ) |
9 |
|
ssiun2 |
|- ( x e. A -> suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) ) |
10 |
|
rankon |
|- ( rank ` x ) e. On |
11 |
10
|
onsuci |
|- suc ( rank ` x ) e. On |
12 |
11
|
rgenw |
|- A. x e. A suc ( rank ` x ) e. On |
13 |
|
iunon |
|- ( ( A e. _V /\ A. x e. A suc ( rank ` x ) e. On ) -> U_ x e. A suc ( rank ` x ) e. On ) |
14 |
1 12 13
|
mp2an |
|- U_ x e. A suc ( rank ` x ) e. On |
15 |
|
r1ord3 |
|- ( ( suc ( rank ` x ) e. On /\ U_ x e. A suc ( rank ` x ) e. On ) -> ( suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) ) ) |
16 |
11 14 15
|
mp2an |
|- ( suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) ) |
17 |
9 16
|
syl |
|- ( x e. A -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) ) |
18 |
17
|
sseld |
|- ( x e. A -> ( x e. ( R1 ` suc ( rank ` x ) ) -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) ) |
19 |
8 18
|
mpi |
|- ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) |
20 |
6 19
|
mpgbir |
|- A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) |
21 |
|
fvex |
|- ( R1 ` U_ x e. A suc ( rank ` x ) ) e. _V |
22 |
21
|
rankss |
|- ( A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) -> ( rank ` A ) C_ ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) ) |
23 |
20 22
|
ax-mp |
|- ( rank ` A ) C_ ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) |
24 |
|
r1ord3 |
|- ( ( U_ x e. A suc ( rank ` x ) e. On /\ y e. On ) -> ( U_ x e. A suc ( rank ` x ) C_ y -> ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) ) ) |
25 |
14 24
|
mpan |
|- ( y e. On -> ( U_ x e. A suc ( rank ` x ) C_ y -> ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) ) ) |
26 |
25
|
ss2rabi |
|- { y e. On | U_ x e. A suc ( rank ` x ) C_ y } C_ { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } |
27 |
|
intss |
|- ( { y e. On | U_ x e. A suc ( rank ` x ) C_ y } C_ { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } -> |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } C_ |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } ) |
28 |
26 27
|
ax-mp |
|- |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } C_ |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } |
29 |
|
rankval2 |
|- ( ( R1 ` U_ x e. A suc ( rank ` x ) ) e. _V -> ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) = |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } ) |
30 |
21 29
|
ax-mp |
|- ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) = |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } |
31 |
|
intmin |
|- ( U_ x e. A suc ( rank ` x ) e. On -> |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } = U_ x e. A suc ( rank ` x ) ) |
32 |
14 31
|
ax-mp |
|- |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } = U_ x e. A suc ( rank ` x ) |
33 |
32
|
eqcomi |
|- U_ x e. A suc ( rank ` x ) = |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } |
34 |
28 30 33
|
3sstr4i |
|- ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) C_ U_ x e. A suc ( rank ` x ) |
35 |
23 34
|
sstri |
|- ( rank ` A ) C_ U_ x e. A suc ( rank ` x ) |
36 |
|
iunss |
|- ( U_ x e. A suc ( rank ` x ) C_ ( rank ` A ) <-> A. x e. A suc ( rank ` x ) C_ ( rank ` A ) ) |
37 |
1
|
rankel |
|- ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) |
38 |
|
rankon |
|- ( rank ` A ) e. On |
39 |
10 38
|
onsucssi |
|- ( ( rank ` x ) e. ( rank ` A ) <-> suc ( rank ` x ) C_ ( rank ` A ) ) |
40 |
37 39
|
sylib |
|- ( x e. A -> suc ( rank ` x ) C_ ( rank ` A ) ) |
41 |
36 40
|
mprgbir |
|- U_ x e. A suc ( rank ` x ) C_ ( rank ` A ) |
42 |
35 41
|
eqssi |
|- ( rank ` A ) = U_ x e. A suc ( rank ` x ) |