Theorem naddcnfcl

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

	Ref	Expression
Assertion	naddcnfcl	|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F oF +o G ) e. S )

Proof

Step	Hyp	Ref	Expression
1		ovres	|- ( ( F e. S /\ G e. S ) -> ( F ( oF +o |` ( S X. S ) ) G ) = ( F oF +o G ) )
2	1	adantl	|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F ( oF +o |` ( S X. S ) ) G ) = ( F oF +o G ) )
3		naddcnff	|- ( ( X e. On /\ S = dom ( _om CNF X ) ) -> ( oF +o |` ( S X. S ) ) : ( S X. S ) --> S )
4	3	fovcdmda	|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F ( oF +o |` ( S X. S ) ) G ) e. S )
5	2 4	eqeltrrd	|- ( ( ( X e. On /\ S = dom ( _om CNF X ) ) /\ ( F e. S /\ G e. S ) ) -> ( F oF +o G ) e. S )