Step |
Hyp |
Ref |
Expression |
1 |
|
r1tr |
|- Tr ( R1 ` suc ( rank ` A ) ) |
2 |
|
rankidb |
|- ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) ) |
3 |
|
trss |
|- ( Tr ( R1 ` suc ( rank ` A ) ) -> ( A e. ( R1 ` suc ( rank ` A ) ) -> A C_ ( R1 ` suc ( rank ` A ) ) ) ) |
4 |
1 2 3
|
mpsyl |
|- ( A e. U. ( R1 " On ) -> A C_ ( R1 ` suc ( rank ` A ) ) ) |
5 |
|
rankdmr1 |
|- ( rank ` A ) e. dom R1 |
6 |
|
r1sucg |
|- ( ( rank ` A ) e. dom R1 -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) ) |
7 |
5 6
|
ax-mp |
|- ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) |
8 |
4 7
|
sseqtrdi |
|- ( A e. U. ( R1 " On ) -> A C_ ~P ( R1 ` ( rank ` A ) ) ) |
9 |
|
sspwuni |
|- ( A C_ ~P ( R1 ` ( rank ` A ) ) <-> U. A C_ ( R1 ` ( rank ` A ) ) ) |
10 |
8 9
|
sylib |
|- ( A e. U. ( R1 " On ) -> U. A C_ ( R1 ` ( rank ` A ) ) ) |
11 |
|
fvex |
|- ( R1 ` ( rank ` A ) ) e. _V |
12 |
11
|
elpw2 |
|- ( U. A e. ~P ( R1 ` ( rank ` A ) ) <-> U. A C_ ( R1 ` ( rank ` A ) ) ) |
13 |
10 12
|
sylibr |
|- ( A e. U. ( R1 " On ) -> U. A e. ~P ( R1 ` ( rank ` A ) ) ) |
14 |
13 7
|
eleqtrrdi |
|- ( A e. U. ( R1 " On ) -> U. A e. ( R1 ` suc ( rank ` A ) ) ) |
15 |
|
r1elwf |
|- ( U. A e. ( R1 ` suc ( rank ` A ) ) -> U. A e. U. ( R1 " On ) ) |
16 |
14 15
|
syl |
|- ( A e. U. ( R1 " On ) -> U. A e. U. ( R1 " On ) ) |
17 |
|
pwwf |
|- ( U. A e. U. ( R1 " On ) <-> ~P U. A e. U. ( R1 " On ) ) |
18 |
|
pwuni |
|- A C_ ~P U. A |
19 |
|
sswf |
|- ( ( ~P U. A e. U. ( R1 " On ) /\ A C_ ~P U. A ) -> A e. U. ( R1 " On ) ) |
20 |
18 19
|
mpan2 |
|- ( ~P U. A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) ) |
21 |
17 20
|
sylbi |
|- ( U. A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) ) |
22 |
16 21
|
impbii |
|- ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) ) |