Theorem ofoacl

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

	Ref	Expression
Assertion	ofoacl	|- ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( F e. ( C ^m A ) /\ G e. ( C ^m A ) ) ) -> ( F oF +o G ) e. ( C ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		ovres	|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m A ) ) -> ( F ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) G ) = ( F oF +o G ) )
2	1	adantl	|- ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( F e. ( C ^m A ) /\ G e. ( C ^m A ) ) ) -> ( F ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) G ) = ( F oF +o G ) )
3		id	|- ( A e. V -> A e. V )
4		inidm	|- ( A i^i A ) = A
5	4	a1i	|- ( A e. V -> ( A i^i A ) = A )
6	5	eqcomd	|- ( A e. V -> A = ( A i^i A ) )
7	3 3 6	3jca	|- ( A e. V -> ( A e. V /\ A e. V /\ A = ( A i^i A ) ) )
8		ofoaf	|- ( ( ( A e. V /\ A e. V /\ A = ( A i^i A ) ) /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) --> ( C ^m A ) )
9	7 8	sylan	|- ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) -> ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) : ( ( C ^m A ) X. ( C ^m A ) ) --> ( C ^m A ) )
10	9	fovcdmda	|- ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( F e. ( C ^m A ) /\ G e. ( C ^m A ) ) ) -> ( F ( oF +o |` ( ( C ^m A ) X. ( C ^m A ) ) ) G ) e. ( C ^m A ) )
11	2 10	eqeltrrd	|- ( ( ( A e. V /\ ( B e. On /\ C = ( _om ^o B ) ) ) /\ ( F e. ( C ^m A ) /\ G e. ( C ^m A ) ) ) -> ( F oF +o G ) e. ( C ^m A ) )