Step |
Hyp |
Ref |
Expression |
1 |
|
rankid.1 |
|- A e. _V |
2 |
|
unir1 |
|- U. ( R1 " On ) = _V |
3 |
1 2
|
eleqtrri |
|- A e. U. ( R1 " On ) |
4 |
|
r1fnon |
|- R1 Fn On |
5 |
|
fndm |
|- ( R1 Fn On -> dom R1 = On ) |
6 |
4 5
|
ax-mp |
|- dom R1 = On |
7 |
6
|
eleq2i |
|- ( B e. dom R1 <-> B e. On ) |
8 |
7
|
biimpri |
|- ( B e. On -> B e. dom R1 ) |
9 |
|
rankr1clem |
|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( -. A e. ( R1 ` B ) <-> B C_ ( rank ` A ) ) ) |
10 |
3 8 9
|
sylancr |
|- ( B e. On -> ( -. A e. ( R1 ` B ) <-> B C_ ( rank ` A ) ) ) |
11 |
10
|
bicomd |
|- ( B e. On -> ( B C_ ( rank ` A ) <-> -. A e. ( R1 ` B ) ) ) |