Metamath Proof Explorer

Theorem ofoaass

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

Ref Expression
Assertion ofoaass ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) = ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 elmapfn ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐹 Fn 𝐴 )
2 1 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐹 Fn 𝐴 )
3 2 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐹 Fn 𝐴 )
4 elmapfn ⊢ ( 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐺 Fn 𝐴 )
5 4 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐺 Fn 𝐴 )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐺 Fn 𝐴 )
7 simpll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐴 ∈ 𝑉 )
8 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
9 3 6 7 7 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o 𝐺 ) Fn 𝐴 )
10 elmapfn ⊢ ( 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐻 Fn 𝐴 )
11 10 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐻 Fn 𝐴 )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐻 Fn 𝐴 )
13 9 12 7 7 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) Fn 𝐴 )
14 6 12 7 7 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( 𝐺 ∘f +o 𝐻 ) Fn 𝐴 )
15 3 14 7 7 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) Fn 𝐴 )
16 simpllr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐵 ∈ On )
17 elmapi ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
18 17 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
20 19 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 )
21 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) ∈ On )
22 16 20 21 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ On )
23 elmapi ⊢ ( 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐺 : 𝐴 ⟶ 𝐵 )
24 23 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐺 : 𝐴 ⟶ 𝐵 )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐺 : 𝐴 ⟶ 𝐵 )
26 25 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ 𝐵 )
27 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝐺 ‘ 𝑎 ) ∈ 𝐵 ) → ( 𝐺 ‘ 𝑎 ) ∈ On )
28 16 26 27 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ On )
29 elmapi ⊢ ( 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) → 𝐻 : 𝐴 ⟶ 𝐵 )
30 29 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
31 30 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
32 31 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑎 ) ∈ 𝐵 )
33 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝐻 ‘ 𝑎 ) ∈ 𝐵 ) → ( 𝐻 ‘ 𝑎 ) ∈ On )
34 16 32 33 syl2anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑎 ) ∈ On )
35 oaass ⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ On ∧ ( 𝐺 ‘ 𝑎 ) ∈ On ∧ ( 𝐻 ‘ 𝑎 ) ∈ On ) → ( ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) +o ( 𝐻 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) ) )
36 22 28 34 35 syl3anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) +o ( 𝐻 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) ) )
37 3 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐹 Fn 𝐴 )
38 6 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐺 Fn 𝐴 )
39 7 anim1i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) )
40 fnfvof ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) )
41 37 38 39 40 syl21anc ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) )
42 41 oveq1d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) = ( ( ( 𝐹 ‘ 𝑎 ) +o ( 𝐺 ‘ 𝑎 ) ) +o ( 𝐻 ‘ 𝑎 ) ) )
43 6 12 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( 𝐺 Fn 𝐴 ∧ 𝐻 Fn 𝐴 ) )
44 fnfvof ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝐻 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) )
45 43 39 44 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑎 ) = ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) )
46 45 oveq2d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) ) )
47 36 42 46 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) = ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑎 ) ) )
48 9 12 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( ( 𝐹 ∘f +o 𝐺 ) Fn 𝐴 ∧ 𝐻 Fn 𝐴 ) )
49 fnfvof ⊢ ( ( ( ( 𝐹 ∘f +o 𝐺 ) Fn 𝐴 ∧ 𝐻 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) ‘ 𝑎 ) = ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) )
50 48 39 49 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) ‘ 𝑎 ) = ( ( ( 𝐹 ∘f +o 𝐺 ) ‘ 𝑎 ) +o ( 𝐻 ‘ 𝑎 ) ) )
51 3 14 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( 𝐹 Fn 𝐴 ∧ ( 𝐺 ∘f +o 𝐻 ) Fn 𝐴 ) )
52 fnfvof ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝐺 ∘f +o 𝐻 ) Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) ) → ( ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑎 ) ) )
53 51 39 52 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) ‘ 𝑎 ) = ( ( 𝐹 ‘ 𝑎 ) +o ( ( 𝐺 ∘f +o 𝐻 ) ‘ 𝑎 ) ) )
54 47 50 53 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) ‘ 𝑎 ) = ( ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) ‘ 𝑎 ) )
55 13 15 54 eqfnfvd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On ) ∧ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐻 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( ( 𝐹 ∘f +o 𝐺 ) ∘f +o 𝐻 ) = ( 𝐹 ∘f +o ( 𝐺 ∘f +o 𝐻 ) ) )