Step |
Hyp |
Ref |
Expression |
1 |
|
rankr1b.1 |
|- A e. _V |
2 |
|
pwuni |
|- A C_ ~P U. A |
3 |
1
|
uniex |
|- U. A e. _V |
4 |
3
|
pwex |
|- ~P U. A e. _V |
5 |
4
|
rankss |
|- ( A C_ ~P U. A -> ( rank ` A ) C_ ( rank ` ~P U. A ) ) |
6 |
2 5
|
ax-mp |
|- ( rank ` A ) C_ ( rank ` ~P U. A ) |
7 |
3
|
rankpw |
|- ( rank ` ~P U. A ) = suc ( rank ` U. A ) |
8 |
6 7
|
sseqtri |
|- ( rank ` A ) C_ suc ( rank ` U. A ) |
9 |
8
|
a1i |
|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` A ) C_ suc ( rank ` U. A ) ) |
10 |
1
|
rankel |
|- ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) |
11 |
|
eleq1 |
|- ( ( rank ` x ) = ( rank ` U. A ) -> ( ( rank ` x ) e. ( rank ` A ) <-> ( rank ` U. A ) e. ( rank ` A ) ) ) |
12 |
10 11
|
syl5ibcom |
|- ( x e. A -> ( ( rank ` x ) = ( rank ` U. A ) -> ( rank ` U. A ) e. ( rank ` A ) ) ) |
13 |
12
|
rexlimiv |
|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` U. A ) e. ( rank ` A ) ) |
14 |
|
rankon |
|- ( rank ` U. A ) e. On |
15 |
|
rankon |
|- ( rank ` A ) e. On |
16 |
14 15
|
onsucssi |
|- ( ( rank ` U. A ) e. ( rank ` A ) <-> suc ( rank ` U. A ) C_ ( rank ` A ) ) |
17 |
13 16
|
sylib |
|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> suc ( rank ` U. A ) C_ ( rank ` A ) ) |
18 |
9 17
|
eqssd |
|- ( E. x e. A ( rank ` x ) = ( rank ` U. A ) -> ( rank ` A ) = suc ( rank ` U. A ) ) |