Theorem ofoacl

Description: Closure law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025)

	Ref	Expression
Assertion	ofoacl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o 𝐺 ) ∈ ( 𝐶 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ovres	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐴 ) ) → ( 𝐹 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝐺 ) = ( 𝐹 ∘f +o 𝐺 ) )
2	1	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( 𝐹 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝐺 ) = ( 𝐹 ∘f +o 𝐺 ) )
3		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
4		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
5	4	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐴 ) = 𝐴 )
6	5	eqcomd	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 = ( 𝐴 ∩ 𝐴 ) )
7	3 3 6	3jca	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 = ( 𝐴 ∩ 𝐴 ) ) )
8		ofoaf	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐴 = ( 𝐴 ∩ 𝐴 ) ) ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ⟶ ( 𝐶 ↑m 𝐴 ) )
9	7 8	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) → ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) : ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ⟶ ( 𝐶 ↑m 𝐴 ) )
10	9	fovcdmda	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( 𝐹 ( ∘f +o ↾ ( ( 𝐶 ↑m 𝐴 ) × ( 𝐶 ↑m 𝐴 ) ) ) 𝐺 ) ∈ ( 𝐶 ↑m 𝐴 ) )
11	2 10	eqeltrrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ On ∧ 𝐶 = ( ω ↑o 𝐵 ) ) ) ∧ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o 𝐺 ) ∈ ( 𝐶 ↑m 𝐴 ) )