ofoafg

Description: Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025)

		Ref	Expression
	Assertion	ofoafg	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to ({\circ_{f} +_{𝑜} ↾}_{((D^{A}) \times (E^{B}))}) : (D^{A}) \times (E^{B}) ⟶ F^{C}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E)) \to D \in On$
2		simp1	$⊢ (A \in V \land B \in W \land C = A \cap B) \to A \in V$
3		elmapg	$⊢ (D \in On \land A \in V) \to (f \in (D^{A}) \leftrightarrow f : A ⟶ D)$
4	1 2 3	syl2anr	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to (f \in (D^{A}) \leftrightarrow f : A ⟶ D)$
5		simp2	$⊢ (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E)) \to E \in On$
6		simp2	$⊢ (A \in V \land B \in W \land C = A \cap B) \to B \in W$
7		elmapg	$⊢ (E \in On \land B \in W) \to (g \in (E^{B}) \leftrightarrow g : B ⟶ E)$
8	5 6 7	syl2anr	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to (g \in (E^{B}) \leftrightarrow g : B ⟶ E)$
9	8	adantr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land f : A ⟶ D) \to (g \in (E^{B}) \leftrightarrow g : B ⟶ E)$
10		simpl	$⊢ (f : A ⟶ D \land g : B ⟶ E) \to f : A ⟶ D$
11	10	ffnd	$⊢ (f : A ⟶ D \land g : B ⟶ E) \to f Fn A$
12	11	adantl	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to f Fn A$
13		simpr	$⊢ (f : A ⟶ D \land g : B ⟶ E) \to g : B ⟶ E$
14	13	ffnd	$⊢ (f : A ⟶ D \land g : B ⟶ E) \to g Fn B$
15	14	adantl	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to g Fn B$
16	2	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to A \in V$
17	6	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to B \in W$
18		eqid	$⊢ A \cap B = A \cap B$
19	12 15 16 17 18	offn	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (f {+_{𝑜}}_{f} g) Fn (A \cap B)$
20		simp3	$⊢ (A \in V \land B \in W \land C = A \cap B) \to C = A \cap B$
21	20	fneq2d	$⊢ (A \in V \land B \in W \land C = A \cap B) \to ((f {+_{𝑜}}_{f} g) Fn C \leftrightarrow (f {+_{𝑜}}_{f} g) Fn (A \cap B))$
22	21	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ((f {+_{𝑜}}_{f} g) Fn C \leftrightarrow (f {+_{𝑜}}_{f} g) Fn (A \cap B))$
23	19 22	mpbird	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (f {+_{𝑜}}_{f} g) Fn C$
24		fresin	$⊢ f : A ⟶ D \to ({f ↾}_{C}) : A \cap C ⟶ D$
25	24	adantr	$⊢ (f : A ⟶ D \land g : B ⟶ E) \to ({f ↾}_{C}) : A \cap C ⟶ D$
26	25	adantl	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({f ↾}_{C}) : A \cap C ⟶ D$
27		inss1	$⊢ A \cap B \subseteq A$
28	20 27	eqsstrdi	$⊢ (A \in V \land B \in W \land C = A \cap B) \to C \subseteq A$
29		sseqin2	$⊢ C \subseteq A \leftrightarrow A \cap C = C$
30	28 29	sylib	$⊢ (A \in V \land B \in W \land C = A \cap B) \to A \cap C = C$
31	30	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to A \cap C = C$
32	31	feq2d	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (({f ↾}_{C}) : A \cap C ⟶ D \leftrightarrow ({f ↾}_{C}) : C ⟶ D)$
33	26 32	mpbid	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({f ↾}_{C}) : C ⟶ D$
34	33	ffvelcdmda	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to ({f ↾}_{C}) (c) \in D$
35	5	ad3antlr	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to E \in On$
36	1	ad3antlr	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to D \in On$
37		onelon	$⊢ (D \in On \land ({f ↾}_{C}) (c) \in D) \to ({f ↾}_{C}) (c) \in On$
38	36 34 37	syl2anc	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to ({f ↾}_{C}) (c) \in On$
39		fresin	$⊢ g : B ⟶ E \to ({g ↾}_{C}) : B \cap C ⟶ E$
40	39	adantl	$⊢ (f : A ⟶ D \land g : B ⟶ E) \to ({g ↾}_{C}) : B \cap C ⟶ E$
41	40	adantl	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({g ↾}_{C}) : B \cap C ⟶ E$
42		inss2	$⊢ A \cap B \subseteq B$
43	20 42	eqsstrdi	$⊢ (A \in V \land B \in W \land C = A \cap B) \to C \subseteq B$
44		sseqin2	$⊢ C \subseteq B \leftrightarrow B \cap C = C$
45	43 44	sylib	$⊢ (A \in V \land B \in W \land C = A \cap B) \to B \cap C = C$
46	45	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to B \cap C = C$
47	46	feq2d	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (({g ↾}_{C}) : B \cap C ⟶ E \leftrightarrow ({g ↾}_{C}) : C ⟶ E)$
48	41 47	mpbid	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({g ↾}_{C}) : C ⟶ E$
49	48	ffvelcdmda	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to ({g ↾}_{C}) (c) \in E$
50		oaordi	$⊢ (E \in On \land ({f ↾}_{C}) (c) \in On) \to (({g ↾}_{C}) (c) \in E \to ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c) \in (({f ↾}_{C}) (c) +_{𝑜} E))$
51	50	imp	$⊢ ((E \in On \land ({f ↾}_{C}) (c) \in On) \land ({g ↾}_{C}) (c) \in E) \to ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c) \in (({f ↾}_{C}) (c) +_{𝑜} E)$
52	35 38 49 51	syl21anc	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c) \in (({f ↾}_{C}) (c) +_{𝑜} E)$
53		oveq1	$⊢ d = ({f ↾}_{C}) (c) \to d +_{𝑜} E = ({f ↾}_{C}) (c) +_{𝑜} E$
54	53	eliuni	$⊢ (({f ↾}_{C}) (c) \in D \land ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c) \in (({f ↾}_{C}) (c) +_{𝑜} E)) \to ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c) \in ⋃_{d \in D} (d +_{𝑜} E)$
55	34 52 54	syl2anc	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c) \in ⋃_{d \in D} (d +_{𝑜} E)$
56	12 15 16 17 18	ofres	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to f {+_{𝑜}}_{f} g = ({f ↾}_{(A \cap B)}) {+_{𝑜}}_{f} ({g ↾}_{(A \cap B)})$
57	20	reseq2d	$⊢ (A \in V \land B \in W \land C = A \cap B) \to {f ↾}_{C} = {f ↾}_{(A \cap B)}$
58	20	reseq2d	$⊢ (A \in V \land B \in W \land C = A \cap B) \to {g ↾}_{C} = {g ↾}_{(A \cap B)}$
59	57 58	oveq12d	$⊢ (A \in V \land B \in W \land C = A \cap B) \to ({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C}) = ({f ↾}_{(A \cap B)}) {+_{𝑜}}_{f} ({g ↾}_{(A \cap B)})$
60	59	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C}) = ({f ↾}_{(A \cap B)}) {+_{𝑜}}_{f} ({g ↾}_{(A \cap B)})$
61	56 60	eqtr4d	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to f {+_{𝑜}}_{f} g = ({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C})$
62	61	fveq1d	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (f {+_{𝑜}}_{f} g) (c) = (({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C})) (c)$
63	62	adantr	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to (f {+_{𝑜}}_{f} g) (c) = (({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C})) (c)$
64	28	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to C \subseteq A$
65	12 64	fnssresd	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({f ↾}_{C}) Fn C$
66	43	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to C \subseteq B$
67	15 66	fnssresd	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ({g ↾}_{C}) Fn C$
68	65 67	jca	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (({f ↾}_{C}) Fn C \land ({g ↾}_{C}) Fn C)$
69		inex1g	$⊢ A \in V \to A \cap B \in V$
70	2 69	syl	$⊢ (A \in V \land B \in W \land C = A \cap B) \to A \cap B \in V$
71	20 70	eqeltrd	$⊢ (A \in V \land B \in W \land C = A \cap B) \to C \in V$
72	71	ad2antrr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to C \in V$
73	72	anim1i	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to (C \in V \land c \in C)$
74		fnfvof	$⊢ ((({f ↾}_{C}) Fn C \land ({g ↾}_{C}) Fn C) \land (C \in V \land c \in C)) \to (({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C})) (c) = ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c)$
75	68 73 74	syl2an2r	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to (({f ↾}_{C}) {+_{𝑜}}_{f} ({g ↾}_{C})) (c) = ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c)$
76	63 75	eqtrd	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to (f {+_{𝑜}}_{f} g) (c) = ({f ↾}_{C}) (c) +_{𝑜} ({g ↾}_{C}) (c)$
77		simp3	$⊢ (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E)) \to F = ⋃_{d \in D} (d +_{𝑜} E)$
78	77	ad3antlr	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to F = ⋃_{d \in D} (d +_{𝑜} E)$
79	55 76 78	3eltr4d	$⊢ ((((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \land c \in C) \to (f {+_{𝑜}}_{f} g) (c) \in F$
80	79	ralrimiva	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to \forall c \in C (f {+_{𝑜}}_{f} g) (c) \in F$
81		fnfvrnss	$⊢ ((f {+_{𝑜}}_{f} g) Fn C \land \forall c \in C (f {+_{𝑜}}_{f} g) (c) \in F) \to ran (f {+_{𝑜}}_{f} g) \subseteq F$
82	80 81	sylan2	$⊢ ((f {+_{𝑜}}_{f} g) Fn C \land (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E))) \to ran (f {+_{𝑜}}_{f} g) \subseteq F$
83	82	expcom	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ((f {+_{𝑜}}_{f} g) Fn C \to ran (f {+_{𝑜}}_{f} g) \subseteq F)$
84	23 83	jcai	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to ((f {+_{𝑜}}_{f} g) Fn C \land ran (f {+_{𝑜}}_{f} g) \subseteq F)$
85		onelon	$⊢ (D \in On \land d \in D) \to d \in On$
86	85	adantlr	$⊢ ((D \in On \land E \in On) \land d \in D) \to d \in On$
87		simpr	$⊢ (D \in On \land E \in On) \to E \in On$
88	87	adantr	$⊢ ((D \in On \land E \in On) \land d \in D) \to E \in On$
89		oacl	$⊢ (d \in On \land E \in On) \to d +_{𝑜} E \in On$
90	86 88 89	syl2anc	$⊢ ((D \in On \land E \in On) \land d \in D) \to d +_{𝑜} E \in On$
91	90	ralrimiva	$⊢ (D \in On \land E \in On) \to \forall d \in D d +_{𝑜} E \in On$
92		iunon	$⊢ (D \in On \land \forall d \in D d +_{𝑜} E \in On) \to ⋃_{d \in D} (d +_{𝑜} E) \in On$
93	91 92	syldan	$⊢ (D \in On \land E \in On) \to ⋃_{d \in D} (d +_{𝑜} E) \in On$
94	93	3adant3	$⊢ (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E)) \to ⋃_{d \in D} (d +_{𝑜} E) \in On$
95	77 94	eqeltrd	$⊢ (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E)) \to F \in On$
96	95	adantl	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to F \in On$
97	96	adantr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to F \in On$
98	97 72	elmapd	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (f {+_{𝑜}}_{f} g \in (F^{C}) \leftrightarrow (f {+_{𝑜}}_{f} g) : C ⟶ F)$
99		df-f	$⊢ (f {+_{𝑜}}_{f} g) : C ⟶ F \leftrightarrow ((f {+_{𝑜}}_{f} g) Fn C \land ran (f {+_{𝑜}}_{f} g) \subseteq F)$
100	98 99	bitrdi	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to (f {+_{𝑜}}_{f} g \in (F^{C}) \leftrightarrow ((f {+_{𝑜}}_{f} g) Fn C \land ran (f {+_{𝑜}}_{f} g) \subseteq F))$
101	84 100	mpbird	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land (f : A ⟶ D \land g : B ⟶ E)) \to f {+_{𝑜}}_{f} g \in (F^{C})$
102	101	expr	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land f : A ⟶ D) \to (g : B ⟶ E \to f {+_{𝑜}}_{f} g \in (F^{C}))$
103	9 102	sylbid	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land f : A ⟶ D) \to (g \in (E^{B}) \to f {+_{𝑜}}_{f} g \in (F^{C}))$
104	103	ralrimiv	$⊢ (((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \land f : A ⟶ D) \to \forall g \in (E^{B}) f {+_{𝑜}}_{f} g \in (F^{C})$
105	104	ex	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to (f : A ⟶ D \to \forall g \in (E^{B}) f {+_{𝑜}}_{f} g \in (F^{C}))$
106	4 105	sylbid	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to (f \in (D^{A}) \to \forall g \in (E^{B}) f {+_{𝑜}}_{f} g \in (F^{C}))$
107	106	ralrimiv	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to \forall f \in (D^{A}) \forall g \in (E^{B}) f {+_{𝑜}}_{f} g \in (F^{C})$
108		ofmres	$⊢ {\circ_{f} +_{𝑜} ↾}_{((D^{A}) \times (E^{B}))} = (f \in (D^{A}), g \in (E^{B}) ⟼ f {+_{𝑜}}_{f} g)$
109	108	fmpo	$⊢ \forall f \in (D^{A}) \forall g \in (E^{B}) f {+_{𝑜}}_{f} g \in (F^{C}) \leftrightarrow ({\circ_{f} +_{𝑜} ↾}_{((D^{A}) \times (E^{B}))}) : (D^{A}) \times (E^{B}) ⟶ F^{C}$
110	107 109	sylib	$⊢ ((A \in V \land B \in W \land C = A \cap B) \land (D \in On \land E \in On \land F = ⋃_{d \in D} (d +_{𝑜} E))) \to ({\circ_{f} +_{𝑜} ↾}_{((D^{A}) \times (E^{B}))}) : (D^{A}) \times (E^{B}) ⟶ F^{C}$

Metamath Proof Explorer

Theorem ofoafg

Proof