Theorem naddcnffn

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

	Ref	Expression
Assertion	naddcnffn	⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		naddcnff	⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) ⟶ 𝑆 )
2	1	ffnd	⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) Fn ( 𝑆 × 𝑆 ) )