Step |
Hyp |
Ref |
Expression |
1 |
|
rankwflemb |
|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) ) |
2 |
|
nfcv |
|- F/_ x R1 |
3 |
|
nfrab1 |
|- F/_ x { x e. On | A e. ( R1 ` suc x ) } |
4 |
3
|
nfint |
|- F/_ x |^| { x e. On | A e. ( R1 ` suc x ) } |
5 |
4
|
nfsuc |
|- F/_ x suc |^| { x e. On | A e. ( R1 ` suc x ) } |
6 |
2 5
|
nffv |
|- F/_ x ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) |
7 |
6
|
nfel2 |
|- F/ x A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) |
8 |
|
suceq |
|- ( x = |^| { x e. On | A e. ( R1 ` suc x ) } -> suc x = suc |^| { x e. On | A e. ( R1 ` suc x ) } ) |
9 |
8
|
fveq2d |
|- ( x = |^| { x e. On | A e. ( R1 ` suc x ) } -> ( R1 ` suc x ) = ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) ) |
10 |
9
|
eleq2d |
|- ( x = |^| { x e. On | A e. ( R1 ` suc x ) } -> ( A e. ( R1 ` suc x ) <-> A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) ) ) |
11 |
7 10
|
onminsb |
|- ( E. x e. On A e. ( R1 ` suc x ) -> A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) ) |
12 |
1 11
|
sylbi |
|- ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) ) |
13 |
|
rankvalb |
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } ) |
14 |
|
suceq |
|- ( ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } -> suc ( rank ` A ) = suc |^| { x e. On | A e. ( R1 ` suc x ) } ) |
15 |
13 14
|
syl |
|- ( A e. U. ( R1 " On ) -> suc ( rank ` A ) = suc |^| { x e. On | A e. ( R1 ` suc x ) } ) |
16 |
15
|
fveq2d |
|- ( A e. U. ( R1 " On ) -> ( R1 ` suc ( rank ` A ) ) = ( R1 ` suc |^| { x e. On | A e. ( R1 ` suc x ) } ) ) |
17 |
12 16
|
eleqtrrd |
|- ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) ) |