ofoaid1

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

		Ref	Expression
	Assertion	ofoaid1	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to F {+_{𝑜}}_{f} (A \times \{\emptyset\}) = F$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to A \in V$
2		onss	$⊢ B \in On \to B \subseteq On$
3		sstr	$⊢ (ran F \subseteq B \land B \subseteq On) \to ran F \subseteq On$
4	3	expcom	$⊢ B \subseteq On \to (ran F \subseteq B \to ran F \subseteq On)$
5	2 4	syl	$⊢ B \in On \to (ran F \subseteq B \to ran F \subseteq On)$
6	5	anim2d	$⊢ B \in On \to ((F Fn A \land ran F \subseteq B) \to (F Fn A \land ran F \subseteq On))$
7		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
8		df-f	$⊢ F : A ⟶ On \leftrightarrow (F Fn A \land ran F \subseteq On)$
9	6 7 8	3imtr4g	$⊢ B \in On \to (F : A ⟶ B \to F : A ⟶ On)$
10		elmapi	$⊢ F \in (B^{A}) \to F : A ⟶ B$
11	9 10	impel	$⊢ (B \in On \land F \in (B^{A})) \to F : A ⟶ On$
12	11	adantll	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to F : A ⟶ On$
13		peano1	$⊢ \emptyset \in ω$
14		fnconstg	$⊢ \emptyset \in ω \to (A \times \{\emptyset\}) Fn A$
15	13 14	mp1i	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to (A \times \{\emptyset\}) Fn A$
16		simp2	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to F : A ⟶ On$
17	16	ffnd	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to F Fn A$
18		simp3	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to (A \times \{\emptyset\}) Fn A$
19		simp1	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to A \in V$
20		inidm	$⊢ A \cap A = A$
21	17 18 19 19 20	offn	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to (F {+_{𝑜}}_{f} (A \times \{\emptyset\})) Fn A$
22	17 18	jca	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to (F Fn A \land (A \times \{\emptyset\}) Fn A)$
23	22	adantr	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to (F Fn A \land (A \times \{\emptyset\}) Fn A)$
24	19	adantr	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to A \in V$
25		simpr	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to a \in A$
26		fnfvof	$⊢ ((F Fn A \land (A \times \{\emptyset\}) Fn A) \land (A \in V \land a \in A)) \to (F {+_{𝑜}}_{f} (A \times \{\emptyset\})) (a) = F (a) +_{𝑜} (A \times \{\emptyset\}) (a)$
27	23 24 25 26	syl12anc	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to (F {+_{𝑜}}_{f} (A \times \{\emptyset\})) (a) = F (a) +_{𝑜} (A \times \{\emptyset\}) (a)$
28		fvconst2g	$⊢ (\emptyset \in ω \land a \in A) \to (A \times \{\emptyset\}) (a) = \emptyset$
29	13 25 28	sylancr	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to (A \times \{\emptyset\}) (a) = \emptyset$
30	29	oveq2d	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to F (a) +_{𝑜} (A \times \{\emptyset\}) (a) = F (a) +_{𝑜} \emptyset$
31	16	ffvelcdmda	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to F (a) \in On$
32		oa0	$⊢ F (a) \in On \to F (a) +_{𝑜} \emptyset = F (a)$
33	31 32	syl	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to F (a) +_{𝑜} \emptyset = F (a)$
34	27 30 33	3eqtrd	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to (F {+_{𝑜}}_{f} (A \times \{\emptyset\})) (a) = F (a)$
35	21 17 34	eqfnfvd	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to F {+_{𝑜}}_{f} (A \times \{\emptyset\}) = F$
36	1 12 15 35	syl3anc	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to F {+_{𝑜}}_{f} (A \times \{\emptyset\}) = F$

Metamath Proof Explorer

Theorem ofoaid1

Proof