ofoaass

Description: Component-wise addition of ordinal-yielding functions is associative. (Contributed by RP, 5-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		elmapfn	$⊢ F \in (B^{A}) \to F Fn A$
2	1	3ad2ant1	$⊢ (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A})) \to F Fn A$
3	2	adantl	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to F Fn A$
4		elmapfn	$⊢ G \in (B^{A}) \to G Fn A$
5	4	3ad2ant2	$⊢ (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A})) \to G Fn A$
6	5	adantl	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to G Fn A$
7		simpll	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to A \in V$
8		inidm	$⊢ A \cap A = A$
9	3 6 7 7 8	offn	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to (F {+_{𝑜}}_{f} G) Fn A$
10		elmapfn	$⊢ H \in (B^{A}) \to H Fn A$
11	10	3ad2ant3	$⊢ (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A})) \to H Fn A$
12	11	adantl	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to H Fn A$
13	9 12 7 7 8	offn	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) Fn A$
14	6 12 7 7 8	offn	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to (G {+_{𝑜}}_{f} H) Fn A$
15	3 14 7 7 8	offn	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) Fn A$
16		simpllr	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to B \in On$
17		elmapi	$⊢ F \in (B^{A}) \to F : A ⟶ B$
18	17	3ad2ant1	$⊢ (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A})) \to F : A ⟶ B$
19	18	adantl	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to F : A ⟶ B$
20	19	ffvelcdmda	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to F (a) \in B$
21		onelon	$⊢ (B \in On \land F (a) \in B) \to F (a) \in On$
22	16 20 21	syl2anc	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to F (a) \in On$
23		elmapi	$⊢ G \in (B^{A}) \to G : A ⟶ B$
24	23	3ad2ant2	$⊢ (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A})) \to G : A ⟶ B$
25	24	adantl	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to G : A ⟶ B$
26	25	ffvelcdmda	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to G (a) \in B$
27		onelon	$⊢ (B \in On \land G (a) \in B) \to G (a) \in On$
28	16 26 27	syl2anc	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to G (a) \in On$
29		elmapi	$⊢ H \in (B^{A}) \to H : A ⟶ B$
30	29	3ad2ant3	$⊢ (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A})) \to H : A ⟶ B$
31	30	adantl	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to H : A ⟶ B$
32	31	ffvelcdmda	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to H (a) \in B$
33		onelon	$⊢ (B \in On \land H (a) \in B) \to H (a) \in On$
34	16 32 33	syl2anc	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to H (a) \in On$
35		oaass	$⊢ (F (a) \in On \land G (a) \in On \land H (a) \in On) \to (F (a) +_{𝑜} G (a)) +_{𝑜} H (a) = F (a) +_{𝑜} (G (a) +_{𝑜} H (a))$
36	22 28 34 35	syl3anc	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (F (a) +_{𝑜} G (a)) +_{𝑜} H (a) = F (a) +_{𝑜} (G (a) +_{𝑜} H (a))$
37	3	adantr	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to F Fn A$
38	6	adantr	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to G Fn A$
39	7	anim1i	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (A \in V \land a \in A)$
40		fnfvof	$⊢ ((F Fn A \land G Fn A) \land (A \in V \land a \in A)) \to (F {+_{𝑜}}_{f} G) (a) = F (a) +_{𝑜} G (a)$
41	37 38 39 40	syl21anc	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (F {+_{𝑜}}_{f} G) (a) = F (a) +_{𝑜} G (a)$
42	41	oveq1d	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (F {+_{𝑜}}_{f} G) (a) +_{𝑜} H (a) = (F (a) +_{𝑜} G (a)) +_{𝑜} H (a)$
43	6 12	jca	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to (G Fn A \land H Fn A)$
44		fnfvof	$⊢ ((G Fn A \land H Fn A) \land (A \in V \land a \in A)) \to (G {+_{𝑜}}_{f} H) (a) = G (a) +_{𝑜} H (a)$
45	43 39 44	syl2an2r	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (G {+_{𝑜}}_{f} H) (a) = G (a) +_{𝑜} H (a)$
46	45	oveq2d	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to F (a) +_{𝑜} (G {+_{𝑜}}_{f} H) (a) = F (a) +_{𝑜} (G (a) +_{𝑜} H (a))$
47	36 42 46	3eqtr4d	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (F {+_{𝑜}}_{f} G) (a) +_{𝑜} H (a) = F (a) +_{𝑜} (G {+_{𝑜}}_{f} H) (a)$
48	9 12	jca	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to ((F {+_{𝑜}}_{f} G) Fn A \land H Fn A)$
49		fnfvof	$⊢ (((F {+_{𝑜}}_{f} G) Fn A \land H Fn A) \land (A \in V \land a \in A)) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) (a) = (F {+_{𝑜}}_{f} G) (a) +_{𝑜} H (a)$
50	48 39 49	syl2an2r	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) (a) = (F {+_{𝑜}}_{f} G) (a) +_{𝑜} H (a)$
51	3 14	jca	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to (F Fn A \land (G {+_{𝑜}}_{f} H) Fn A)$
52		fnfvof	$⊢ ((F Fn A \land (G {+_{𝑜}}_{f} H) Fn A) \land (A \in V \land a \in A)) \to (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) (a) = F (a) +_{𝑜} (G {+_{𝑜}}_{f} H) (a)$
53	51 39 52	syl2an2r	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) (a) = F (a) +_{𝑜} (G {+_{𝑜}}_{f} H) (a)$
54	47 50 53	3eqtr4d	$⊢ (((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \land a \in A) \to ((F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H) (a) = (F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)) (a)$
55	13 15 54	eqfnfvd	$⊢ ((A \in V \land B \in On) \land (F \in (B^{A}) \land G \in (B^{A}) \land H \in (B^{A}))) \to (F {+_{𝑜}}_{f} G) {+_{𝑜}}_{f} H = F {+_{𝑜}}_{f} (G {+_{𝑜}}_{f} H)$

Metamath Proof Explorer

Theorem ofoaass

Proof