Theorem naddcnfcl

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

	Ref	Expression
Assertion	naddcnfcl	⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o 𝐺 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ovres	⊢ ( ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) → ( 𝐹 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝐺 ) = ( 𝐹 ∘f +o 𝐺 ) )
2	1	adantl	⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝐺 ) = ( 𝐹 ∘f +o 𝐺 ) )
3		naddcnff	⊢ ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) → ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) : ( 𝑆 × 𝑆 ) ⟶ 𝑆 )
4	3	fovcdmda	⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ( ∘f +o ↾ ( 𝑆 × 𝑆 ) ) 𝐺 ) ∈ 𝑆 )
5	2 4	eqeltrrd	⊢ ( ( ( 𝑋 ∈ On ∧ 𝑆 = dom ( ω CNF 𝑋 ) ) ∧ ( 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ) ) → ( 𝐹 ∘f +o 𝐺 ) ∈ 𝑆 )