Step |
Hyp |
Ref |
Expression |
1 |
|
pwfseqlem4.g |
|- ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) |
2 |
|
pwfseqlem4.x |
|- ( ph -> X C_ A ) |
3 |
|
pwfseqlem4.h |
|- ( ph -> H : _om -1-1-onto-> X ) |
4 |
|
pwfseqlem4.ps |
|- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) ) |
5 |
|
pwfseqlem4.k |
|- ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x ) |
6 |
|
pwfseqlem4.d |
|- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) |
7 |
|
pwfseqlem4.f |
|- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
8 |
|
oveq1 |
|- ( a = Y -> ( a F s ) = ( Y F s ) ) |
9 |
|
2fveq3 |
|- ( a = Y -> ( H ` ( card ` a ) ) = ( H ` ( card ` Y ) ) ) |
10 |
8 9
|
eqeq12d |
|- ( a = Y -> ( ( a F s ) = ( H ` ( card ` a ) ) <-> ( Y F s ) = ( H ` ( card ` Y ) ) ) ) |
11 |
|
oveq2 |
|- ( s = R -> ( Y F s ) = ( Y F R ) ) |
12 |
11
|
eqeq1d |
|- ( s = R -> ( ( Y F s ) = ( H ` ( card ` Y ) ) <-> ( Y F R ) = ( H ` ( card ` Y ) ) ) ) |
13 |
|
nfcv |
|- F/_ x a |
14 |
|
nfcv |
|- F/_ r a |
15 |
|
nfcv |
|- F/_ r s |
16 |
|
nfmpo1 |
|- F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
17 |
7 16
|
nfcxfr |
|- F/_ x F |
18 |
|
nfcv |
|- F/_ x r |
19 |
13 17 18
|
nfov |
|- F/_ x ( a F r ) |
20 |
19
|
nfeq1 |
|- F/ x ( a F r ) = ( H ` ( card ` a ) ) |
21 |
|
nfmpo2 |
|- F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
22 |
7 21
|
nfcxfr |
|- F/_ r F |
23 |
14 22 15
|
nfov |
|- F/_ r ( a F s ) |
24 |
23
|
nfeq1 |
|- F/ r ( a F s ) = ( H ` ( card ` a ) ) |
25 |
|
oveq1 |
|- ( x = a -> ( x F r ) = ( a F r ) ) |
26 |
|
2fveq3 |
|- ( x = a -> ( H ` ( card ` x ) ) = ( H ` ( card ` a ) ) ) |
27 |
25 26
|
eqeq12d |
|- ( x = a -> ( ( x F r ) = ( H ` ( card ` x ) ) <-> ( a F r ) = ( H ` ( card ` a ) ) ) ) |
28 |
|
oveq2 |
|- ( r = s -> ( a F r ) = ( a F s ) ) |
29 |
28
|
eqeq1d |
|- ( r = s -> ( ( a F r ) = ( H ` ( card ` a ) ) <-> ( a F s ) = ( H ` ( card ` a ) ) ) ) |
30 |
|
vex |
|- x e. _V |
31 |
|
vex |
|- r e. _V |
32 |
|
fvex |
|- ( H ` ( card ` x ) ) e. _V |
33 |
|
fvex |
|- ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. _V |
34 |
32 33
|
ifex |
|- if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) e. _V |
35 |
7
|
ovmpt4g |
|- ( ( x e. _V /\ r e. _V /\ if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) e. _V ) -> ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
36 |
30 31 34 35
|
mp3an |
|- ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) |
37 |
|
iftrue |
|- ( x e. Fin -> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) = ( H ` ( card ` x ) ) ) |
38 |
36 37
|
eqtrid |
|- ( x e. Fin -> ( x F r ) = ( H ` ( card ` x ) ) ) |
39 |
38
|
adantr |
|- ( ( x e. Fin /\ r e. V ) -> ( x F r ) = ( H ` ( card ` x ) ) ) |
40 |
13 14 15 20 24 27 29 39
|
vtocl2gaf |
|- ( ( a e. Fin /\ s e. V ) -> ( a F s ) = ( H ` ( card ` a ) ) ) |
41 |
10 12 40
|
vtocl2ga |
|- ( ( Y e. Fin /\ R e. V ) -> ( Y F R ) = ( H ` ( card ` Y ) ) ) |