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 
|- ( ( ( A e. V /\ B e. On ) /\ ( F e. ( B ^m A ) /\ G e. ( B ^m A ) /\ H e. ( B ^m A ) ) ) -> ( ( F oF +o G ) oF +o H ) = ( F oF +o ( G oF +o H ) ) )

Proof

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