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 ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) –onto→ 𝑆 )

Proof

Step Hyp Ref Expression
1 naddcnff ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) ⟶ 𝑆 )
2 simpr ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝑓 ∈ 𝑆 ) → 𝑓 ∈ 𝑆 )
3 peano1 ⊢ ∅ ∈ ω
4 fconst6g ⊢ ( ∅ ∈ ω → ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω )
5 3 4 mp1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω )
6 simpl ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑋 ∈ On )
7 3 a1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ∅ ∈ ω )
8 6 7 fczfsuppd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑋 × { ∅ } ) finSupp ∅ )
9 simpr ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → 𝑆 = dom ( ω CNF 𝑋 ) )
10 9 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ↔ ( 𝑋 × { ∅ } ) ∈ dom ( ω CNF 𝑋 ) ) )
11 eqid ⊢ dom ( ω CNF 𝑋 ) = dom ( ω CNF 𝑋 )
12 omelon ⊢ ω ∈ On
13 12 a1i ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ω ∈ On )
14 11 13 6 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑋 × { ∅ } ) ∈ dom ( ω CNF 𝑋 ) ↔ ( ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω ∧ ( 𝑋 × { ∅ } ) finSupp ∅ ) ) )
15 10 14 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝑋 × { ∅ } ) : 𝑋 ⟶ ω ∧ ( 𝑋 × { ∅ } ) finSupp ∅ ) ) )
16 5 8 15 mpbir2and ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑋 × { ∅ } ) ∈ 𝑆 )
17 16 adantr ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝑓 ∈ 𝑆 ) → ( 𝑋 × { ∅ } ) ∈ 𝑆 )
18 simpl ⊢ ( ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → 𝑓 ∈ 𝑆 )
19 18 adantl ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → 𝑓 ∈ 𝑆 )
20 simpr ⊢ ( ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → ( 𝑋 × { ∅ } ) ∈ 𝑆 )
21 20 adantl ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → ( 𝑋 × { ∅ } ) ∈ 𝑆 )
22 19 21 ovresd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) ( 𝑋 × { ∅ } ) ) = ( 𝑓 ∘f +o ( 𝑋 × { ∅ } ) ) )
23 9 eleq2d ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ 𝑆 ↔ 𝑓 ∈ dom ( ω CNF 𝑋 ) ) )
24 11 13 6 cantnfs ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) )
25 23 24 bitrd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ 𝑆 ↔ ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) )
26 25 biimpd ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( 𝑓 ∈ 𝑆 → ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) ) )
27 simpl ⊢ ( ( 𝑓 : 𝑋 ⟶ ω ∧ 𝑓 finSupp ∅ ) → 𝑓 : 𝑋 ⟶ ω )
28 18 26 27 syl56 ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) → 𝑓 : 𝑋 ⟶ ω ) )
29 28 imp ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → 𝑓 : 𝑋 ⟶ ω )
30 29 ffnd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → 𝑓 Fn 𝑋 )
31 fnconstg ⊢ ( ∅ ∈ ω → ( 𝑋 × { ∅ } ) Fn 𝑋 )
32 3 31 mp1i ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → ( 𝑋 × { ∅ } ) Fn 𝑋 )
33 6 adantr ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → 𝑋 ∈ On )
34 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
35 30 32 33 33 34 offn ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → ( 𝑓 ∘f +o ( 𝑋 × { ∅ } ) ) Fn 𝑋 )
36 30 adantr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑓 Fn 𝑋 )
37 3 31 mp1i ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 × { ∅ } ) Fn 𝑋 )
38 simplll ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ On )
39 simpr ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
40 fnfvof ⊢ ( ( ( 𝑓 Fn 𝑋 ∧ ( 𝑋 × { ∅ } ) Fn 𝑋 ) ∧ ( 𝑋 ∈ On ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑓 ∘f +o ( 𝑋 × { ∅ } ) ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) +o ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) ) )
41 36 37 38 39 40 syl22anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ∘f +o ( 𝑋 × { ∅ } ) ) ‘ 𝑥 ) = ( ( 𝑓 ‘ 𝑥 ) +o ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) ) )
42 3 a1i ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∅ ∈ ω )
43 fvconst2g ⊢ ( ( ∅ ∈ ω ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) = ∅ )
44 42 39 43 syl2anc ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) = ∅ )
45 44 oveq2d ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ‘ 𝑥 ) +o ( ( 𝑋 × { ∅ } ) ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) +o ∅ ) )
46 29 ffvelcdmda ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑥 ) ∈ ω )
47 nnon ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ω → ( 𝑓 ‘ 𝑥 ) ∈ On )
48 oa0 ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ On → ( ( 𝑓 ‘ 𝑥 ) +o ∅ ) = ( 𝑓 ‘ 𝑥 ) )
49 46 47 48 3syl ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ‘ 𝑥 ) +o ∅ ) = ( 𝑓 ‘ 𝑥 ) )
50 41 45 49 3eqtrd ⊢ ( ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑓 ∘f +o ( 𝑋 × { ∅ } ) ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
51 35 30 50 eqfnfvd ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → ( 𝑓 ∘f +o ( 𝑋 × { ∅ } ) ) = 𝑓 )
52 22 51 eqtr2d ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝑓 ∈ 𝑆 ∧ ( 𝑋 × { ∅ } ) ∈ 𝑆 ) ) → 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) ( 𝑋 × { ∅ } ) ) )
53 52 expr ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝑓 ∈ 𝑆 ) → ( ( 𝑋 × { ∅ } ) ∈ 𝑆 → 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) ( 𝑋 × { ∅ } ) ) ) )
54 17 53 jcai ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝑓 ∈ 𝑆 ) → ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ∧ 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) ( 𝑋 × { ∅ } ) ) ) )
55 oveq2 ⊢ ( 𝑧 = ( 𝑋 × { ∅ } ) → ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) ( 𝑋 × { ∅ } ) ) )
56 55 rspceeqv ⊢ ( ( ( 𝑋 × { ∅ } ) ∈ 𝑆 ∧ 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) ( 𝑋 × { ∅ } ) ) ) → ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
57 54 56 syl ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝑓 ∈ 𝑆 ) → ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
58 oveq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
59 58 eqeq2d ⊢ ( 𝑔 = 𝑓 → ( 𝑓 = ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ↔ 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
60 59 rexbidv ⊢ ( 𝑔 = 𝑓 → ( ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ↔ ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
61 60 rspcev ⊢ ( ( 𝑓 ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑓 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) → ∃ 𝑔 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
62 2 57 61 syl2anc ⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ 𝑓 ∈ 𝑆 ) → ∃ 𝑔 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
63 62 ralrimiva ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ∀ 𝑓 ∈ 𝑆 ∃ 𝑔 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) )
64 foov ⊢ ( ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) –onto→ 𝑆 ↔ ( ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) ⟶ 𝑆 ∧ ∀ 𝑓 ∈ 𝑆 ∃ 𝑔 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 𝑓 = ( 𝑔 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝑧 ) ) )
65 1 63 64 sylanbrc ⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) –onto→ 𝑆 )