Step |
Hyp |
Ref |
Expression |
1 |
|
cantnffval.s |
|- S = { g e. ( A ^m B ) | g finSupp (/) } |
2 |
|
cantnffval.a |
|- ( ph -> A e. On ) |
3 |
|
cantnffval.b |
|- ( ph -> B e. On ) |
4 |
1 2 3
|
cantnffval |
|- ( ph -> ( A CNF B ) = ( f e. S |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) ) |
5 |
4
|
dmeqd |
|- ( ph -> dom ( A CNF B ) = dom ( f e. S |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) ) |
6 |
|
fvex |
|- ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V |
7 |
6
|
csbex |
|- [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V |
8 |
7
|
rgenw |
|- A. f e. S [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V |
9 |
|
dmmptg |
|- ( A. f e. S [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V -> dom ( f e. S |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) = S ) |
10 |
8 9
|
ax-mp |
|- dom ( f e. S |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) = S |
11 |
5 10
|
eqtrdi |
|- ( ph -> dom ( A CNF B ) = S ) |