Step |
Hyp |
Ref |
Expression |
1 |
|
rankidn |
|- ( A e. U. ( R1 " On ) -> -. A e. ( R1 ` ( rank ` A ) ) ) |
2 |
|
rankon |
|- ( rank ` A ) e. On |
3 |
|
r1suc |
|- ( ( rank ` A ) e. On -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) ) |
4 |
2 3
|
ax-mp |
|- ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) |
5 |
4
|
eleq2i |
|- ( ~P A e. ( R1 ` suc ( rank ` A ) ) <-> ~P A e. ~P ( R1 ` ( rank ` A ) ) ) |
6 |
|
elpwi |
|- ( ~P A e. ~P ( R1 ` ( rank ` A ) ) -> ~P A C_ ( R1 ` ( rank ` A ) ) ) |
7 |
|
pwidg |
|- ( A e. U. ( R1 " On ) -> A e. ~P A ) |
8 |
|
ssel |
|- ( ~P A C_ ( R1 ` ( rank ` A ) ) -> ( A e. ~P A -> A e. ( R1 ` ( rank ` A ) ) ) ) |
9 |
6 7 8
|
syl2imc |
|- ( A e. U. ( R1 " On ) -> ( ~P A e. ~P ( R1 ` ( rank ` A ) ) -> A e. ( R1 ` ( rank ` A ) ) ) ) |
10 |
5 9
|
syl5bi |
|- ( A e. U. ( R1 " On ) -> ( ~P A e. ( R1 ` suc ( rank ` A ) ) -> A e. ( R1 ` ( rank ` A ) ) ) ) |
11 |
1 10
|
mtod |
|- ( A e. U. ( R1 " On ) -> -. ~P A e. ( R1 ` suc ( rank ` A ) ) ) |
12 |
|
r1rankidb |
|- ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) ) |
13 |
12
|
sspwd |
|- ( A e. U. ( R1 " On ) -> ~P A C_ ~P ( R1 ` ( rank ` A ) ) ) |
14 |
13 4
|
sseqtrrdi |
|- ( A e. U. ( R1 " On ) -> ~P A C_ ( R1 ` suc ( rank ` A ) ) ) |
15 |
|
fvex |
|- ( R1 ` suc ( rank ` A ) ) e. _V |
16 |
15
|
elpw2 |
|- ( ~P A e. ~P ( R1 ` suc ( rank ` A ) ) <-> ~P A C_ ( R1 ` suc ( rank ` A ) ) ) |
17 |
14 16
|
sylibr |
|- ( A e. U. ( R1 " On ) -> ~P A e. ~P ( R1 ` suc ( rank ` A ) ) ) |
18 |
2
|
onsuci |
|- suc ( rank ` A ) e. On |
19 |
|
r1suc |
|- ( suc ( rank ` A ) e. On -> ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) ) ) |
20 |
18 19
|
ax-mp |
|- ( R1 ` suc suc ( rank ` A ) ) = ~P ( R1 ` suc ( rank ` A ) ) |
21 |
17 20
|
eleqtrrdi |
|- ( A e. U. ( R1 " On ) -> ~P A e. ( R1 ` suc suc ( rank ` A ) ) ) |
22 |
|
pwwf |
|- ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) ) |
23 |
|
rankr1c |
|- ( ~P A e. U. ( R1 " On ) -> ( suc ( rank ` A ) = ( rank ` ~P A ) <-> ( -. ~P A e. ( R1 ` suc ( rank ` A ) ) /\ ~P A e. ( R1 ` suc suc ( rank ` A ) ) ) ) ) |
24 |
22 23
|
sylbi |
|- ( A e. U. ( R1 " On ) -> ( suc ( rank ` A ) = ( rank ` ~P A ) <-> ( -. ~P A e. ( R1 ` suc ( rank ` A ) ) /\ ~P A e. ( R1 ` suc suc ( rank ` A ) ) ) ) ) |
25 |
11 21 24
|
mpbir2and |
|- ( A e. U. ( R1 " On ) -> suc ( rank ` A ) = ( rank ` ~P A ) ) |
26 |
25
|
eqcomd |
|- ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) ) |