Metamath Proof Explorer

Theorem naddcnffo

Description: Addition of Cantor normal forms is a function onto Cantor normal forms. (Contributed by RP, 2-Jan-2025)

Ref Expression
Assertion naddcnffo 
|- ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( oF +o |` ( S X. S ) ) : ( S X. S ) -onto-> S )

Proof

Step Hyp Ref Expression
1 naddcnff 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( oF +o |` ( S X. S ) ) : ( S X. S ) --> S )
2 simpr 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ f e. S ) -> f e. S )
3 peano1 
 |-  (/) e. _om
4 fconst6g 
 |-  ( (/) e. _om -> ( X X. { (/) } ) : X --> _om )
5 3 4 mp1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) : X --> _om )
6 simpl 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> X e. On )
7 3 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> (/) e. _om )
8 6 7 fczfsuppd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) finSupp (/) )
9 simpr 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> S = dom ( _om CNF X ) )
10 9 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. S <-> ( X X. { (/) } ) e. dom ( _om CNF X ) ) )
11 eqid 
 |-  dom ( _om CNF X ) = dom ( _om CNF X )
12 omelon 
 |-  _om e. On
13 12 a1i 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> _om e. On )
14 11 13 6 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. dom ( _om CNF X ) <-> ( ( X X. { (/) } ) : X --> _om /\ ( X X. { (/) } ) finSupp (/) ) ) )
15 10 14 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( X X. { (/) } ) e. S <-> ( ( X X. { (/) } ) : X --> _om /\ ( X X. { (/) } ) finSupp (/) ) ) )
16 5 8 15 mpbir2and 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( X X. { (/) } ) e. S )
17 16 adantr 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ f e. S ) -> ( X X. { (/) } ) e. S )
18 simpl 
 |-  ( ( f e. S /\ ( X X. { (/) } ) e. S ) -> f e. S )
19 18 adantl 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> f e. S )
20 simpr 
 |-  ( ( f e. S /\ ( X X. { (/) } ) e. S ) -> ( X X. { (/) } ) e. S )
21 20 adantl 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> ( X X. { (/) } ) e. S )
22 19 21 ovresd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> ( f ( oF +o |` ( S X. S ) ) ( X X. { (/) } ) ) = ( f oF +o ( X X. { (/) } ) ) )
23 9 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( f e. S <-> f e. dom ( _om CNF X ) ) )
24 11 13 6 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( f e. dom ( _om CNF X ) <-> ( f : X --> _om /\ f finSupp (/) ) ) )
25 23 24 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( f e. S <-> ( f : X --> _om /\ f finSupp (/) ) ) )
26 25 biimpd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( f e. S -> ( f : X --> _om /\ f finSupp (/) ) ) )
27 simpl 
 |-  ( ( f : X --> _om /\ f finSupp (/) ) -> f : X --> _om )
28 18 26 27 syl56 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( f e. S /\ ( X X. { (/) } ) e. S ) -> f : X --> _om ) )
29 28 imp 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> f : X --> _om )
30 29 ffnd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> f Fn X )
31 fnconstg 
 |-  ( (/) e. _om -> ( X X. { (/) } ) Fn X )
32 3 31 mp1i 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> ( X X. { (/) } ) Fn X )
33 6 adantr 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> X e. On )
34 inidm 
 |-  ( X i^i X ) = X
35 30 32 33 33 34 offn 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> ( f oF +o ( X X. { (/) } ) ) Fn X )
36 30 adantr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> f Fn X )
37 3 31 mp1i 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> ( X X. { (/) } ) Fn X )
38 simplll 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> X e. On )
39 simpr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> x e. X )
40 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 ) ) )
41 36 37 38 39 40 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 ) ) )
42 3 a1i 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> (/) e. _om )
43 fvconst2g 
 |-  ( ( (/) e. _om /\ x e. X ) -> ( ( X X. { (/) } ) ` x ) = (/) )
44 42 39 43 syl2anc 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> ( ( X X. { (/) } ) ` x ) = (/) )
45 44 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 (/) ) )
46 29 ffvelcdmda 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> ( f ` x ) e. _om )
47 nnon 
 |-  ( ( f ` x ) e. _om -> ( f ` x ) e. On )
48 oa0 
 |-  ( ( f ` x ) e. On -> ( ( f ` x ) +o (/) ) = ( f ` x ) )
49 46 47 48 3syl 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) /\ x e. X ) -> ( ( f ` x ) +o (/) ) = ( f ` x ) )
50 41 45 49 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 ) )
51 35 30 50 eqfnfvd 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> ( f oF +o ( X X. { (/) } ) ) = f )
52 22 51 eqtr2d 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f e. S /\ ( X X. { (/) } ) e. S ) ) -> f = ( f ( oF +o |` ( S X. S ) ) ( X X. { (/) } ) ) )
53 52 expr 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ f e. S ) -> ( ( X X. { (/) } ) e. S -> f = ( f ( oF +o |` ( S X. S ) ) ( X X. { (/) } ) ) ) )
54 17 53 jcai 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ f e. S ) -> ( ( X X. { (/) } ) e. S /\ f = ( f ( oF +o |` ( S X. S ) ) ( X X. { (/) } ) ) ) )
55 oveq2 
 |-  ( z = ( X X. { (/) } ) -> ( f ( oF +o |` ( S X. S ) ) z ) = ( f ( oF +o |` ( S X. S ) ) ( X X. { (/) } ) ) )
56 55 rspceeqv 
 |-  ( ( ( X X. { (/) } ) e. S /\ f = ( f ( oF +o |` ( S X. S ) ) ( X X. { (/) } ) ) ) -> E. z e. S f = ( f ( oF +o |` ( S X. S ) ) z ) )
57 54 56 syl 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ f e. S ) -> E. z e. S f = ( f ( oF +o |` ( S X. S ) ) z ) )
58 oveq1 
 |-  ( g = f -> ( g ( oF +o |` ( S X. S ) ) z ) = ( f ( oF +o |` ( S X. S ) ) z ) )
59 58 eqeq2d 
 |-  ( g = f -> ( f = ( g ( oF +o |` ( S X. S ) ) z ) <-> f = ( f ( oF +o |` ( S X. S ) ) z ) ) )
60 59 rexbidv 
 |-  ( g = f -> ( E. z e. S f = ( g ( oF +o |` ( S X. S ) ) z ) <-> E. z e. S f = ( f ( oF +o |` ( S X. S ) ) z ) ) )
61 60 rspcev 
 |-  ( ( f e. S /\ E. z e. S f = ( f ( oF +o |` ( S X. S ) ) z ) ) -> E. g e. S E. z e. S f = ( g ( oF +o |` ( S X. S ) ) z ) )
62 2 57 61 syl2anc 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ f e. S ) -> E. g e. S E. z e. S f = ( g ( oF +o |` ( S X. S ) ) z ) )
63 62 ralrimiva 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> A. f e. S E. g e. S E. z e. S f = ( g ( oF +o |` ( S X. S ) ) z ) )
64 foov 
 |-  ( ( oF +o |` ( S X. S ) ) : ( S X. S ) -onto-> S <-> ( ( oF +o |` ( S X. S ) ) : ( S X. S ) --> S /\ A. f e. S E. g e. S E. z e. S f = ( g ( oF +o |` ( S X. S ) ) z ) ) )
65 1 63 64 sylanbrc 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( oF +o |` ( S X. S ) ) : ( S X. S ) -onto-> S )