naddcnfcl

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

		Ref	Expression
	Assertion	naddcnfcl	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F {+_{𝑜}}_{f} G \in S$

Step	Hyp	Ref	Expression
1		ovres	$⊢ (F \in S \land G \in S) \to F ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) G = F {+_{𝑜}}_{f} G$
2	1	adantl	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) G = F {+_{𝑜}}_{f} G$
3		naddcnff	$⊢ (X \in On \land S = dom (ω CNF X)) \to ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) : S \times S ⟶ S$
4	3	fovcdmda	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F ({\circ_{f} +_{𝑜} ↾}_{(S \times S)}) G \in S$
5	2 4	eqeltrrd	$⊢ ((X \in On \land S = dom (ω CNF X)) \land (F \in S \land G \in S)) \to F {+_{𝑜}}_{f} G \in S$

Metamath Proof Explorer