Step |
Hyp |
Ref |
Expression |
1 |
|
unieq |
|- ( x = A -> U. x = U. A ) |
2 |
1
|
fveq2d |
|- ( x = A -> ( rank ` U. x ) = ( rank ` U. A ) ) |
3 |
|
fveq2 |
|- ( x = A -> ( rank ` x ) = ( rank ` A ) ) |
4 |
3
|
unieqd |
|- ( x = A -> U. ( rank ` x ) = U. ( rank ` A ) ) |
5 |
2 4
|
eqeq12d |
|- ( x = A -> ( ( rank ` U. x ) = U. ( rank ` x ) <-> ( rank ` U. A ) = U. ( rank ` A ) ) ) |
6 |
|
vex |
|- x e. _V |
7 |
6
|
rankuni2 |
|- ( rank ` U. x ) = U_ z e. x ( rank ` z ) |
8 |
|
fvex |
|- ( rank ` z ) e. _V |
9 |
8
|
dfiun2 |
|- U_ z e. x ( rank ` z ) = U. { y | E. z e. x y = ( rank ` z ) } |
10 |
7 9
|
eqtri |
|- ( rank ` U. x ) = U. { y | E. z e. x y = ( rank ` z ) } |
11 |
|
df-rex |
|- ( E. z e. x y = ( rank ` z ) <-> E. z ( z e. x /\ y = ( rank ` z ) ) ) |
12 |
6
|
rankel |
|- ( z e. x -> ( rank ` z ) e. ( rank ` x ) ) |
13 |
12
|
anim1i |
|- ( ( z e. x /\ y = ( rank ` z ) ) -> ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) ) |
14 |
13
|
eximi |
|- ( E. z ( z e. x /\ y = ( rank ` z ) ) -> E. z ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) ) |
15 |
|
19.42v |
|- ( E. z ( y e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) ) |
16 |
|
eleq1 |
|- ( y = ( rank ` z ) -> ( y e. ( rank ` x ) <-> ( rank ` z ) e. ( rank ` x ) ) ) |
17 |
16
|
pm5.32ri |
|- ( ( y e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) ) |
18 |
17
|
exbii |
|- ( E. z ( y e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> E. z ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) ) |
19 |
|
simpl |
|- ( ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) -> y e. ( rank ` x ) ) |
20 |
|
rankon |
|- ( rank ` x ) e. On |
21 |
20
|
oneli |
|- ( y e. ( rank ` x ) -> y e. On ) |
22 |
|
r1fnon |
|- R1 Fn On |
23 |
|
fndm |
|- ( R1 Fn On -> dom R1 = On ) |
24 |
22 23
|
ax-mp |
|- dom R1 = On |
25 |
21 24
|
eleqtrrdi |
|- ( y e. ( rank ` x ) -> y e. dom R1 ) |
26 |
|
rankr1id |
|- ( y e. dom R1 <-> ( rank ` ( R1 ` y ) ) = y ) |
27 |
25 26
|
sylib |
|- ( y e. ( rank ` x ) -> ( rank ` ( R1 ` y ) ) = y ) |
28 |
27
|
eqcomd |
|- ( y e. ( rank ` x ) -> y = ( rank ` ( R1 ` y ) ) ) |
29 |
|
fvex |
|- ( R1 ` y ) e. _V |
30 |
|
fveq2 |
|- ( z = ( R1 ` y ) -> ( rank ` z ) = ( rank ` ( R1 ` y ) ) ) |
31 |
30
|
eqeq2d |
|- ( z = ( R1 ` y ) -> ( y = ( rank ` z ) <-> y = ( rank ` ( R1 ` y ) ) ) ) |
32 |
29 31
|
spcev |
|- ( y = ( rank ` ( R1 ` y ) ) -> E. z y = ( rank ` z ) ) |
33 |
28 32
|
syl |
|- ( y e. ( rank ` x ) -> E. z y = ( rank ` z ) ) |
34 |
33
|
ancli |
|- ( y e. ( rank ` x ) -> ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) ) |
35 |
19 34
|
impbii |
|- ( ( y e. ( rank ` x ) /\ E. z y = ( rank ` z ) ) <-> y e. ( rank ` x ) ) |
36 |
15 18 35
|
3bitr3i |
|- ( E. z ( ( rank ` z ) e. ( rank ` x ) /\ y = ( rank ` z ) ) <-> y e. ( rank ` x ) ) |
37 |
14 36
|
sylib |
|- ( E. z ( z e. x /\ y = ( rank ` z ) ) -> y e. ( rank ` x ) ) |
38 |
11 37
|
sylbi |
|- ( E. z e. x y = ( rank ` z ) -> y e. ( rank ` x ) ) |
39 |
38
|
abssi |
|- { y | E. z e. x y = ( rank ` z ) } C_ ( rank ` x ) |
40 |
39
|
unissi |
|- U. { y | E. z e. x y = ( rank ` z ) } C_ U. ( rank ` x ) |
41 |
10 40
|
eqsstri |
|- ( rank ` U. x ) C_ U. ( rank ` x ) |
42 |
|
pwuni |
|- x C_ ~P U. x |
43 |
|
vuniex |
|- U. x e. _V |
44 |
43
|
pwex |
|- ~P U. x e. _V |
45 |
44
|
rankss |
|- ( x C_ ~P U. x -> ( rank ` x ) C_ ( rank ` ~P U. x ) ) |
46 |
42 45
|
ax-mp |
|- ( rank ` x ) C_ ( rank ` ~P U. x ) |
47 |
43
|
rankpw |
|- ( rank ` ~P U. x ) = suc ( rank ` U. x ) |
48 |
46 47
|
sseqtri |
|- ( rank ` x ) C_ suc ( rank ` U. x ) |
49 |
48
|
unissi |
|- U. ( rank ` x ) C_ U. suc ( rank ` U. x ) |
50 |
|
rankon |
|- ( rank ` U. x ) e. On |
51 |
50
|
onunisuci |
|- U. suc ( rank ` U. x ) = ( rank ` U. x ) |
52 |
49 51
|
sseqtri |
|- U. ( rank ` x ) C_ ( rank ` U. x ) |
53 |
41 52
|
eqssi |
|- ( rank ` U. x ) = U. ( rank ` x ) |
54 |
5 53
|
vtoclg |
|- ( A e. _V -> ( rank ` U. A ) = U. ( rank ` A ) ) |
55 |
|
uniexb |
|- ( A e. _V <-> U. A e. _V ) |
56 |
|
fvprc |
|- ( -. U. A e. _V -> ( rank ` U. A ) = (/) ) |
57 |
55 56
|
sylnbi |
|- ( -. A e. _V -> ( rank ` U. A ) = (/) ) |
58 |
|
uni0 |
|- U. (/) = (/) |
59 |
57 58
|
eqtr4di |
|- ( -. A e. _V -> ( rank ` U. A ) = U. (/) ) |
60 |
|
fvprc |
|- ( -. A e. _V -> ( rank ` A ) = (/) ) |
61 |
60
|
unieqd |
|- ( -. A e. _V -> U. ( rank ` A ) = U. (/) ) |
62 |
59 61
|
eqtr4d |
|- ( -. A e. _V -> ( rank ` U. A ) = U. ( rank ` A ) ) |
63 |
54 62
|
pm2.61i |
|- ( rank ` U. A ) = U. ( rank ` A ) |