Metamath Proof Explorer

Theorem cantnfdm

Description: The domain of the Cantor normal form function (in later lemmas we will use dom ( A CNF B ) to abbreviate "the set of finitely supported functions from B to A "). (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnffval.s 
|- S = { g e. ( A ^m B ) | g finSupp (/) }
cantnffval.a 
|- ( ph -> A e. On )
cantnffval.b 
|- ( ph -> B e. On )
Assertion cantnfdm 
|- ( ph -> dom ( A CNF B ) = S )

Proof

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 )