Metamath Proof Explorer

Theorem naddcnff

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

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

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 1 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( g e. S <-> g e. dom ( _om CNF X ) ) )
10 3 5 6 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( g e. dom ( _om CNF X ) <-> ( g : X --> _om /\ g finSupp (/) ) ) )
11 9 10 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( g e. S <-> ( g : X --> _om /\ g finSupp (/) ) ) )
12 11 adantr 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) -> ( g e. S <-> ( g : X --> _om /\ g finSupp (/) ) ) )
13 simpl 
 |-  ( ( f : X --> _om /\ f finSupp (/) ) -> f : X --> _om )
14 simpl 
 |-  ( ( g : X --> _om /\ g finSupp (/) ) -> g : X --> _om )
15 13 14 anim12i 
 |-  ( ( ( f : X --> _om /\ f finSupp (/) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( f : X --> _om /\ g : X --> _om ) )
16 6 15 anim12i 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( ( f : X --> _om /\ f finSupp (/) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) ) -> ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) )
17 16 anassrs 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) )
18 simprl 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> f : X --> _om )
19 18 ffnd 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> f Fn X )
20 simprr 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> g : X --> _om )
21 20 ffnd 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> g Fn X )
22 simpl 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> X e. On )
23 inidm 
 |-  ( X i^i X ) = X
24 19 21 22 22 23 offn 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> ( f oF +o g ) Fn X )
25 simpr 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ ( f oF +o g ) Fn X ) -> ( f oF +o g ) Fn X )
26 simplrl 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> f : X --> _om )
27 26 ffnd 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> f Fn X )
28 simplrr 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> g : X --> _om )
29 28 ffnd 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> g Fn X )
30 simpll 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> X e. On )
31 simpr 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> x e. X )
32 fnfvof 
 |-  ( ( ( f Fn X /\ g Fn X ) /\ ( X e. On /\ x e. X ) ) -> ( ( f oF +o g ) ` x ) = ( ( f ` x ) +o ( g ` x ) ) )
33 27 29 30 31 32 syl22anc 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> ( ( f oF +o g ) ` x ) = ( ( f ` x ) +o ( g ` x ) ) )
34 18 ffvelcdmda 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> ( f ` x ) e. _om )
35 20 ffvelcdmda 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> ( g ` x ) e. _om )
36 nnacl 
 |-  ( ( ( f ` x ) e. _om /\ ( g ` x ) e. _om ) -> ( ( f ` x ) +o ( g ` x ) ) e. _om )
37 34 35 36 syl2anc 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> ( ( f ` x ) +o ( g ` x ) ) e. _om )
38 33 37 eqeltrd 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ x e. X ) -> ( ( f oF +o g ) ` x ) e. _om )
39 38 ex 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> ( x e. X -> ( ( f oF +o g ) ` x ) e. _om ) )
40 39 ralrimiv 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> A. x e. X ( ( f oF +o g ) ` x ) e. _om )
41 40 adantr 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ ( f oF +o g ) Fn X ) -> A. x e. X ( ( f oF +o g ) ` x ) e. _om )
42 fnfvrnss 
 |-  ( ( ( f oF +o g ) Fn X /\ A. x e. X ( ( f oF +o g ) ` x ) e. _om ) -> ran ( f oF +o g ) C_ _om )
43 25 41 42 syl2anc 
 |-  ( ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) /\ ( f oF +o g ) Fn X ) -> ran ( f oF +o g ) C_ _om )
44 43 ex 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> ( ( f oF +o g ) Fn X -> ran ( f oF +o g ) C_ _om ) )
45 24 44 jcai 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> ( ( f oF +o g ) Fn X /\ ran ( f oF +o g ) C_ _om ) )
46 df-f 
 |-  ( ( f oF +o g ) : X --> _om <-> ( ( f oF +o g ) Fn X /\ ran ( f oF +o g ) C_ _om ) )
47 45 46 sylibr 
 |-  ( ( X e. On /\ ( f : X --> _om /\ g : X --> _om ) ) -> ( f oF +o g ) : X --> _om )
48 17 47 syl 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( f oF +o g ) : X --> _om )
49 ffun 
 |-  ( ( f oF +o g ) : X --> _om -> Fun ( f oF +o g ) )
50 49 adantl 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> Fun ( f oF +o g ) )
51 simplrr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> f finSupp (/) )
52 51 adantr 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> f finSupp (/) )
53 simplrr 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> g finSupp (/) )
54 52 53 fsuppunfi 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( ( f supp (/) ) u. ( g supp (/) ) ) e. Fin )
55 simp-4l 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> X e. On )
56 peano1 
 |-  (/) e. _om
57 56 a1i 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> (/) e. _om )
58 simplrl 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> f : X --> _om )
59 58 adantr 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> f : X --> _om )
60 simplrl 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> g : X --> _om )
61 0elon 
 |-  (/) e. On
62 oa0 
 |-  ( (/) e. On -> ( (/) +o (/) ) = (/) )
63 61 62 mp1i 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( (/) +o (/) ) = (/) )
64 55 57 59 60 63 suppofssd 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( ( f oF +o g ) supp (/) ) C_ ( ( f supp (/) ) u. ( g supp (/) ) ) )
65 54 64 ssfid 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( ( f oF +o g ) supp (/) ) e. Fin )
66 ovexd 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( f oF +o g ) e. _V )
67 isfsupp 
 |-  ( ( ( f oF +o g ) e. _V /\ (/) e. On ) -> ( ( f oF +o g ) finSupp (/) <-> ( Fun ( f oF +o g ) /\ ( ( f oF +o g ) supp (/) ) e. Fin ) ) )
68 66 61 67 sylancl 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( ( f oF +o g ) finSupp (/) <-> ( Fun ( f oF +o g ) /\ ( ( f oF +o g ) supp (/) ) e. Fin ) ) )
69 50 65 68 mpbir2and 
 |-  ( ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) /\ ( f oF +o g ) : X --> _om ) -> ( f oF +o g ) finSupp (/) )
70 69 ex 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( ( f oF +o g ) : X --> _om -> ( f oF +o g ) finSupp (/) ) )
71 48 70 jcai 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( ( f oF +o g ) : X --> _om /\ ( f oF +o g ) finSupp (/) ) )
72 1 eleq2d 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( f oF +o g ) e. S <-> ( f oF +o g ) e. dom ( _om CNF X ) ) )
73 3 5 6 cantnfs 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( f oF +o g ) e. dom ( _om CNF X ) <-> ( ( f oF +o g ) : X --> _om /\ ( f oF +o g ) finSupp (/) ) ) )
74 72 73 bitrd 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( f oF +o g ) e. S <-> ( ( f oF +o g ) : X --> _om /\ ( f oF +o g ) finSupp (/) ) ) )
75 74 ad2antrr 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( ( f oF +o g ) e. S <-> ( ( f oF +o g ) : X --> _om /\ ( f oF +o g ) finSupp (/) ) ) )
76 71 75 mpbird 
 |-  ( ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) /\ ( g : X --> _om /\ g finSupp (/) ) ) -> ( f oF +o g ) e. S )
77 76 ex 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) -> ( ( g : X --> _om /\ g finSupp (/) ) -> ( f oF +o g ) e. S ) )
78 12 77 sylbid 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) -> ( g e. S -> ( f oF +o g ) e. S ) )
79 78 ralrimiv 
 |-  ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( f : X --> _om /\ f finSupp (/) ) ) -> A. g e. S ( f oF +o g ) e. S )
80 79 ex 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( ( f : X --> _om /\ f finSupp (/) ) -> A. g e. S ( f oF +o g ) e. S ) )
81 8 80 sylbid 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( f e. S -> A. g e. S ( f oF +o g ) e. S ) )
82 81 ralrimiv 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> A. f e. S A. g e. S ( f oF +o g ) e. S )
83 ofmres 
 |-  ( oF +o |` ( S X. S ) ) = ( f e. S , g e. S |-> ( f oF +o g ) )
84 83 fmpo 
 |-  ( A. f e. S A. g e. S ( f oF +o g ) e. S <-> ( oF +o |` ( S X. S ) ) : ( S X. S ) --> S )
85 82 84 sylib 
 |-  ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( oF +o |` ( S X. S ) ) : ( S X. S ) --> S )