Metamath Proof Explorer

Theorem naddcnfid1

Description: Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 fconst6g 
 |-  ( (/) e. _om -> ( X X. { (/) } ) : X --> _om )
3 1 2 mp1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) : X --> _om )
4 simpl 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> X e. On )
5 1 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> (/) e. _om )
6 4 5 fczfsuppd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) finSupp (/) )
7 simpr 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> S = dom ( _om CNF X ) )
8 7 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. S <-> ( X X. { (/) } ) e. dom ( _om CNF X ) ) )
9 eqid 
 |-  dom ( _om CNF X ) = dom ( _om CNF X )
10 omelon 
 |-  _om e. On
11 10 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> _om e. On )
12 9 11 4 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. dom ( _om CNF X ) <-> ( ( X X. { (/) } ) : X --> _om /\ ( X X. { (/) } ) finSupp (/) ) ) )
13 8 12 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. S <-> ( ( X X. { (/) } ) : X --> _om /\ ( X X. { (/) } ) finSupp (/) ) ) )
14 3 6 13 mpbir2and 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) e. S )
15 7 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. S <-> F e. dom ( _om CNF X ) ) )
16 9 11 4 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. dom ( _om CNF X ) <-> ( F : X --> _om /\ F finSupp (/) ) ) )
17 15 16 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( F e. S <-> ( F : X --> _om /\ F finSupp (/) ) ) )
18 17 simprbda 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> F : X --> _om )
19 18 ffnd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> F Fn X )
20 19 adantr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) -> F Fn X )
21 2 ffnd 
 |-  ( (/) e. _om -> ( X X. { (/) } ) Fn X )
22 1 21 mp1i 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) -> ( X X. { (/) } ) Fn X )
23 simplll 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) -> X e. On )
24 inidm 
 |-  ( X i^i X ) = X
25 20 22 23 23 24 offn 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) -> ( F oF +o ( X X. { (/) } ) ) Fn X )
26 20 adantr 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> F Fn X )
27 1 21 mp1i 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( X X. { (/) } ) Fn X )
28 simp-4l 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> X e. On )
29 simpr 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> x e. X )
30 fnfvof 
 |-  ( ( ( F Fn X /\ ( X X. { (/) } ) Fn X ) /\ ( X e. On /\ x e. X ) ) -> ( ( F oF +o ( X X. { (/) } ) ) ` x ) = ( ( F ` x ) +o ( ( X X. { (/) } ) ` x ) ) )
31 26 27 28 29 30 syl22anc 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( ( F oF +o ( X X. { (/) } ) ) ` x ) = ( ( F ` x ) +o ( ( X X. { (/) } ) ` x ) ) )
32 fvconst2g 
 |-  ( ( (/) e. _om /\ x e. X ) -> ( ( X X. { (/) } ) ` x ) = (/) )
33 1 29 32 sylancr 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( ( X X. { (/) } ) ` x ) = (/) )
34 33 oveq2d 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( ( F ` x ) +o ( ( X X. { (/) } ) ` x ) ) = ( ( F ` x ) +o (/) ) )
35 18 adantr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) -> F : X --> _om )
36 35 ffvelcdmda 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( F ` x ) e. _om )
37 nna0 
 |-  ( ( F ` x ) e. _om -> ( ( F ` x ) +o (/) ) = ( F ` x ) )
38 36 37 syl 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( ( F ` x ) +o (/) ) = ( F ` x ) )
39 31 34 38 3eqtrd 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) /\ x e. X ) -> ( ( F oF +o ( X X. { (/) } ) ) ` x ) = ( F ` x ) )
40 25 20 39 eqfnfvd 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) /\ ( X X. { (/) } ) e. S ) -> ( F oF +o ( X X. { (/) } ) ) = F )
41 14 40 mpidan 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ F e. S ) -> ( F oF +o ( X X. { (/) } ) ) = F )