Step |
Hyp |
Ref |
Expression |
1 |
|
infxpenc2.1 |
|- ( ph -> A e. On ) |
2 |
|
infxpenc2.2 |
|- ( ph -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) |
3 |
|
infxpenc2.3 |
|- W = ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) ) |
4 |
|
infxpenc2.4 |
|- ( ph -> F : ( _om ^o 2o ) -1-1-onto-> _om ) |
5 |
|
infxpenc2.5 |
|- ( ph -> ( F ` (/) ) = (/) ) |
6 |
|
infxpenc2.k |
|- K = ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) ) |
7 |
|
infxpenc2.h |
|- H = ( ( ( _om CNF W ) o. K ) o. `' ( ( _om ^o 2o ) CNF W ) ) |
8 |
|
infxpenc2.l |
|- L = ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) ) |
9 |
|
infxpenc2.x |
|- X = ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) |
10 |
|
infxpenc2.y |
|- Y = ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) |
11 |
|
infxpenc2.j |
|- J = ( ( ( _om CNF ( 2o .o W ) ) o. L ) o. `' ( _om CNF ( W .o 2o ) ) ) |
12 |
|
infxpenc2.z |
|- Z = ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) ) |
13 |
|
infxpenc2.t |
|- T = ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. ) |
14 |
|
infxpenc2.g |
|- G = ( `' ( n ` b ) o. ( ( ( H o. J ) o. Z ) o. T ) ) |
15 |
1
|
mptexd |
|- ( ph -> ( b e. A |-> G ) e. _V ) |
16 |
1
|
adantr |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> A e. On ) |
17 |
|
simprl |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> b e. A ) |
18 |
|
onelon |
|- ( ( A e. On /\ b e. A ) -> b e. On ) |
19 |
16 17 18
|
syl2anc |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> b e. On ) |
20 |
|
simprr |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> _om C_ b ) |
21 |
1 2 3
|
infxpenc2lem1 |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( W e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) ) |
22 |
21
|
simpld |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> W e. ( On \ 1o ) ) |
23 |
4
|
adantr |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> F : ( _om ^o 2o ) -1-1-onto-> _om ) |
24 |
5
|
adantr |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( F ` (/) ) = (/) ) |
25 |
21
|
simprd |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) |
26 |
19 20 22 23 24 25 6 7 8 9 10 11 12 13 14
|
infxpenc |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> G : ( b X. b ) -1-1-onto-> b ) |
27 |
|
f1of |
|- ( G : ( b X. b ) -1-1-onto-> b -> G : ( b X. b ) --> b ) |
28 |
26 27
|
syl |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> G : ( b X. b ) --> b ) |
29 |
|
vex |
|- b e. _V |
30 |
29 29
|
xpex |
|- ( b X. b ) e. _V |
31 |
|
fex |
|- ( ( G : ( b X. b ) --> b /\ ( b X. b ) e. _V ) -> G e. _V ) |
32 |
28 30 31
|
sylancl |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> G e. _V ) |
33 |
|
eqid |
|- ( b e. A |-> G ) = ( b e. A |-> G ) |
34 |
33
|
fvmpt2 |
|- ( ( b e. A /\ G e. _V ) -> ( ( b e. A |-> G ) ` b ) = G ) |
35 |
17 32 34
|
syl2anc |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( ( b e. A |-> G ) ` b ) = G ) |
36 |
35
|
f1oeq1d |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b <-> G : ( b X. b ) -1-1-onto-> b ) ) |
37 |
26 36
|
mpbird |
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) |
38 |
37
|
expr |
|- ( ( ph /\ b e. A ) -> ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) |
39 |
38
|
ralrimiva |
|- ( ph -> A. b e. A ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) |
40 |
|
nfmpt1 |
|- F/_ b ( b e. A |-> G ) |
41 |
40
|
nfeq2 |
|- F/ b g = ( b e. A |-> G ) |
42 |
|
fveq1 |
|- ( g = ( b e. A |-> G ) -> ( g ` b ) = ( ( b e. A |-> G ) ` b ) ) |
43 |
42
|
f1oeq1d |
|- ( g = ( b e. A |-> G ) -> ( ( g ` b ) : ( b X. b ) -1-1-onto-> b <-> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) |
44 |
43
|
imbi2d |
|- ( g = ( b e. A |-> G ) -> ( ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) <-> ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) ) |
45 |
41 44
|
ralbid |
|- ( g = ( b e. A |-> G ) -> ( A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) <-> A. b e. A ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) ) |
46 |
15 39 45
|
spcedv |
|- ( ph -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) ) |