ofoaid2

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

		Ref	Expression
	Assertion	ofoaid2	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to (A \times \{\emptyset\}) {+_{𝑜}}_{f} F = 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		simp3	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to (A \times \{\emptyset\}) Fn A$
17		simp2	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to F : A ⟶ On$
18	17	ffnd	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to F 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	16 18 19 19 20	offn	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to ((A \times \{\emptyset\}) {+_{𝑜}}_{f} F) Fn A$
22	16 18	jca	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to ((A \times \{\emptyset\}) Fn A \land F Fn A)$
23	22	adantr	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to ((A \times \{\emptyset\}) Fn A \land F 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	$⊢ (((A \times \{\emptyset\}) Fn A \land F Fn A) \land (A \in V \land a \in A)) \to ((A \times \{\emptyset\}) {+_{𝑜}}_{f} F) (a) = (A \times \{\emptyset\}) (a) +_{𝑜} F (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 ((A \times \{\emptyset\}) {+_{𝑜}}_{f} F) (a) = (A \times \{\emptyset\}) (a) +_{𝑜} F (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	oveq1d	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to (A \times \{\emptyset\}) (a) +_{𝑜} F (a) = \emptyset +_{𝑜} F (a)$
31	17	ffvelcdmda	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to F (a) \in On$
32		oa0r	$⊢ F (a) \in On \to \emptyset +_{𝑜} F (a) = F (a)$
33	31 32	syl	$⊢ ((A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \land a \in A) \to \emptyset +_{𝑜} F (a) = 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 ((A \times \{\emptyset\}) {+_{𝑜}}_{f} F) (a) = F (a)$
35	21 18 34	eqfnfvd	$⊢ (A \in V \land F : A ⟶ On \land (A \times \{\emptyset\}) Fn A) \to (A \times \{\emptyset\}) {+_{𝑜}}_{f} F = F$
36	1 12 15 35	syl3anc	$⊢ ((A \in V \land B \in On) \land F \in (B^{A})) \to (A \times \{\emptyset\}) {+_{𝑜}}_{f} F = F$

Metamath Proof Explorer

Theorem ofoaid2

Proof