Metamath Proof Explorer

Theorem naddcnfcom

Description: Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025)

Ref Expression
Assertion naddcnfcom 
|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F oF +o G ) = ( G oF +o F ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> S = dom ( _om CNF X ) )
2 1 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. S <-> F e. dom ( _om CNF X ) ) )
3 eqid 
 |-  dom ( _om CNF X ) = dom ( _om CNF X )
4 omelon 
 |-  _om e. On
5 4 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> _om e. On )
6 simpl 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> X e. On )
7 3 5 6 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. dom ( _om CNF X ) <-> ( F : X --> _om /\ F finSupp (/) ) ) )
8 2 7 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. S <-> ( F : X --> _om /\ F finSupp (/) ) ) )
9 simpl 
 |-  ( ( F : X --> _om /\ F finSupp (/) ) -> F : X --> _om )
10 8 9 syl6bi 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. S -> F : X --> _om ) )
11 simpl 
 |-  ( ( F e. S /\ G e. S ) -> F e. S )
12 10 11 impel 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> F : X --> _om )
13 12 ffnd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> F Fn X )
14 1 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( G e. S <-> G e. dom ( _om CNF X ) ) )
15 3 5 6 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( G e. dom ( _om CNF X ) <-> ( G : X --> _om /\ G finSupp (/) ) ) )
16 14 15 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( G e. S <-> ( G : X --> _om /\ G finSupp (/) ) ) )
17 simpl 
 |-  ( ( G : X --> _om /\ G finSupp (/) ) -> G : X --> _om )
18 16 17 syl6bi 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( G e. S -> G : X --> _om ) )
19 simpr 
 |-  ( ( F e. S /\ G e. S ) -> G e. S )
20 18 19 impel 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> G : X --> _om )
21 20 ffnd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> G Fn X )
22 simpll 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> X e. On )
23 inidm 
 |-  ( X i^i X ) = X
24 13 21 22 22 23 offn 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F oF +o G ) Fn X )
25 21 13 22 22 23 offn 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( G oF +o F ) Fn X )
26 12 ffvelcdmda 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> ( F ` x ) e. _om )
27 20 ffvelcdmda 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> ( G ` x ) e. _om )
28 nnacom 
 |-  ( ( ( F ` x ) e. _om /\ ( G ` x ) e. _om ) -> ( ( F ` x ) +o ( G ` x ) ) = ( ( G ` x ) +o ( F ` x ) ) )
29 26 27 28 syl2anc 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> ( ( F ` x ) +o ( G ` x ) ) = ( ( G ` x ) +o ( F ` x ) ) )
30 13 adantr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> F Fn X )
31 21 adantr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> G Fn X )
32 simplll 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> X e. On )
33 simpr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> x e. X )
34 fnfvof 
 |-  ( ( ( F Fn X /\ G Fn X ) /\ ( X e. On /\ x e. X ) ) -> ( ( F oF +o G ) ` x ) = ( ( F ` x ) +o ( G ` x ) ) )
35 30 31 32 33 34 syl22anc 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> ( ( F oF +o G ) ` x ) = ( ( F ` x ) +o ( G ` x ) ) )
36 fnfvof 
 |-  ( ( ( G Fn X /\ F Fn X ) /\ ( X e. On /\ x e. X ) ) -> ( ( G oF +o F ) ` x ) = ( ( G ` x ) +o ( F ` x ) ) )
37 31 30 32 33 36 syl22anc 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> ( ( G oF +o F ) ` x ) = ( ( G ` x ) +o ( F ` x ) ) )
38 29 35 37 3eqtr4d 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) /\ x e. X ) -> ( ( F oF +o G ) ` x ) = ( ( G oF +o F ) ` x ) )
39 24 25 38 eqfnfvd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F oF +o G ) = ( G oF +o F ) )