Metamath Proof Explorer

Theorem cantnffval

Description: The value of the Cantor normal form function. (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 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 ) ) )

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 oveq12 
 |-  ( ( x = A /\ y = B ) -> ( x ^m y ) = ( A ^m B ) )
5 4 rabeqdv 
 |-  ( ( x = A /\ y = B ) -> { g e. ( x ^m y ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) } )
6 5 1 eqtr4di 
 |-  ( ( x = A /\ y = B ) -> { g e. ( x ^m y ) | g finSupp (/) } = S )
7 simp1l 
 |-  ( ( ( x = A /\ y = B ) /\ k e. _V /\ z e. _V ) -> x = A )
8 7 oveq1d 
 |-  ( ( ( x = A /\ y = B ) /\ k e. _V /\ z e. _V ) -> ( x ^o ( h ` k ) ) = ( A ^o ( h ` k ) ) )
9 8 oveq1d 
 |-  ( ( ( x = A /\ y = B ) /\ k e. _V /\ z e. _V ) -> ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) = ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) )
10 9 oveq1d 
 |-  ( ( ( x = A /\ y = B ) /\ k e. _V /\ z e. _V ) -> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) = ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) )
11 10 mpoeq3dva 
 |-  ( ( x = A /\ y = B ) -> ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) )
12 eqid 
 |-  (/) = (/)
13 seqomeq12 
 |-  ( ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) /\ (/) = (/) ) -> seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) )
14 11 12 13 sylancl 
 |-  ( ( x = A /\ y = B ) -> seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) )
15 14 fveq1d 
 |-  ( ( x = A /\ y = B ) -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) )
16 15 csbeq2dv 
 |-  ( ( x = A /\ y = B ) -> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) = [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) )
17 6 16 mpteq12dv 
 |-  ( ( x = A /\ y = B ) -> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) = ( 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 ) ) )
18 df-cnf 
 |-  CNF = ( x e. On , y e. On |-> ( f e. { g e. ( x ^m y ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( x ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
19 ovex 
 |-  ( A ^m B ) e. _V
20 1 19 rabex2 
 |-  S e. _V
21 20 mptex 
 |-  ( 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
22 17 18 21 ovmpoa 
 |-  ( ( A e. On /\ B e. On ) -> ( 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 ) ) )
23 2 3 22 syl2anc 
 |-  ( 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 ) ) )