ofoacl

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

		Ref	Expression
	Assertion	ofoacl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (F \in (C^{A}) \land G \in (C^{A}))) \to F {+_{𝑜}}_{f} G \in (C^{A})$

Step	Hyp	Ref	Expression
1		ovres	$⊢ (F \in (C^{A}) \land G \in (C^{A})) \to F ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) G = F {+_{𝑜}}_{f} G$
2	1	adantl	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (F \in (C^{A}) \land G \in (C^{A}))) \to F ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) G = F {+_{𝑜}}_{f} G$
3		id	$⊢ A \in V \to A \in V$
4		inidm	$⊢ A \cap A = A$
5	4	a1i	$⊢ A \in V \to A \cap A = A$
6	5	eqcomd	$⊢ A \in V \to A = A \cap A$
7	3 3 6	3jca	$⊢ A \in V \to (A \in V \land A \in V \land A = A \cap A)$
8		ofoaf	$⊢ ((A \in V \land A \in V \land A = A \cap A) \land (B \in On \land C = ω ↑_{𝑜} B)) \to ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) ⟶ C^{A}$
9	7 8	sylan	$⊢ (A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \to ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) : (C^{A}) \times (C^{A}) ⟶ C^{A}$
10	9	fovcdmda	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (F \in (C^{A}) \land G \in (C^{A}))) \to F ({\circ_{f} +_{𝑜} ↾}_{((C^{A}) \times (C^{A}))}) G \in (C^{A})$
11	2 10	eqeltrrd	$⊢ ((A \in V \land (B \in On \land C = ω ↑_{𝑜} B)) \land (F \in (C^{A}) \land G \in (C^{A}))) \to F {+_{𝑜}}_{f} G \in (C^{A})$

Metamath Proof Explorer