Metamath Proof Explorer

Theorem naddass

Description: Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddass 
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = x -> ( a +no b ) = ( x +no b ) )
2 1 oveq1d 
 |-  ( a = x -> ( ( a +no b ) +no c ) = ( ( x +no b ) +no c ) )
3 oveq1 
 |-  ( a = x -> ( a +no ( b +no c ) ) = ( x +no ( b +no c ) ) )
4 2 3 eqeq12d 
 |-  ( a = x -> ( ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) <-> ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) ) )
5 oveq2 
 |-  ( b = y -> ( x +no b ) = ( x +no y ) )
6 5 oveq1d 
 |-  ( b = y -> ( ( x +no b ) +no c ) = ( ( x +no y ) +no c ) )
7 oveq1 
 |-  ( b = y -> ( b +no c ) = ( y +no c ) )
8 7 oveq2d 
 |-  ( b = y -> ( x +no ( b +no c ) ) = ( x +no ( y +no c ) ) )
9 6 8 eqeq12d 
 |-  ( b = y -> ( ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) <-> ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) ) )
10 oveq2 
 |-  ( c = z -> ( ( x +no y ) +no c ) = ( ( x +no y ) +no z ) )
11 oveq2 
 |-  ( c = z -> ( y +no c ) = ( y +no z ) )
12 11 oveq2d 
 |-  ( c = z -> ( x +no ( y +no c ) ) = ( x +no ( y +no z ) ) )
13 10 12 eqeq12d 
 |-  ( c = z -> ( ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) )
14 oveq1 
 |-  ( a = x -> ( a +no y ) = ( x +no y ) )
15 14 oveq1d 
 |-  ( a = x -> ( ( a +no y ) +no z ) = ( ( x +no y ) +no z ) )
16 oveq1 
 |-  ( a = x -> ( a +no ( y +no z ) ) = ( x +no ( y +no z ) ) )
17 15 16 eqeq12d 
 |-  ( a = x -> ( ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) )
18 oveq2 
 |-  ( b = y -> ( a +no b ) = ( a +no y ) )
19 18 oveq1d 
 |-  ( b = y -> ( ( a +no b ) +no z ) = ( ( a +no y ) +no z ) )
20 oveq1 
 |-  ( b = y -> ( b +no z ) = ( y +no z ) )
21 20 oveq2d 
 |-  ( b = y -> ( a +no ( b +no z ) ) = ( a +no ( y +no z ) ) )
22 19 21 eqeq12d 
 |-  ( b = y -> ( ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) <-> ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) ) )
23 5 oveq1d 
 |-  ( b = y -> ( ( x +no b ) +no z ) = ( ( x +no y ) +no z ) )
24 20 oveq2d 
 |-  ( b = y -> ( x +no ( b +no z ) ) = ( x +no ( y +no z ) ) )
25 23 24 eqeq12d 
 |-  ( b = y -> ( ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) <-> ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) ) )
26 oveq2 
 |-  ( c = z -> ( ( a +no y ) +no c ) = ( ( a +no y ) +no z ) )
27 11 oveq2d 
 |-  ( c = z -> ( a +no ( y +no c ) ) = ( a +no ( y +no z ) ) )
28 26 27 eqeq12d 
 |-  ( c = z -> ( ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) <-> ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) ) )
29 oveq1 
 |-  ( a = A -> ( a +no b ) = ( A +no b ) )
30 29 oveq1d 
 |-  ( a = A -> ( ( a +no b ) +no c ) = ( ( A +no b ) +no c ) )
31 oveq1 
 |-  ( a = A -> ( a +no ( b +no c ) ) = ( A +no ( b +no c ) ) )
32 30 31 eqeq12d 
 |-  ( a = A -> ( ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) <-> ( ( A +no b ) +no c ) = ( A +no ( b +no c ) ) ) )
33 oveq2 
 |-  ( b = B -> ( A +no b ) = ( A +no B ) )
34 33 oveq1d 
 |-  ( b = B -> ( ( A +no b ) +no c ) = ( ( A +no B ) +no c ) )
35 oveq1 
 |-  ( b = B -> ( b +no c ) = ( B +no c ) )
36 35 oveq2d 
 |-  ( b = B -> ( A +no ( b +no c ) ) = ( A +no ( B +no c ) ) )
37 34 36 eqeq12d 
 |-  ( b = B -> ( ( ( A +no b ) +no c ) = ( A +no ( b +no c ) ) <-> ( ( A +no B ) +no c ) = ( A +no ( B +no c ) ) ) )
38 oveq2 
 |-  ( c = C -> ( ( A +no B ) +no c ) = ( ( A +no B ) +no C ) )
39 oveq2 
 |-  ( c = C -> ( B +no c ) = ( B +no C ) )
40 39 oveq2d 
 |-  ( c = C -> ( A +no ( B +no c ) ) = ( A +no ( B +no C ) ) )
41 38 40 eqeq12d 
 |-  ( c = C -> ( ( ( A +no B ) +no c ) = ( A +no ( B +no c ) ) <-> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) ) )
42 simpr21 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) )
43 eleq1 
 |-  ( ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) -> ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) )
44 43 ralimi 
 |-  ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) -> A. x e. a ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) )
45 ralbi 
 |-  ( A. x e. a ( ( ( x +no b ) +no c ) e. w <-> ( x +no ( b +no c ) ) e. w ) -> ( A. x e. a ( ( x +no b ) +no c ) e. w <-> A. x e. a ( x +no ( b +no c ) ) e. w ) )
46 42 44 45 3syl 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. x e. a ( ( x +no b ) +no c ) e. w <-> A. x e. a ( x +no ( b +no c ) ) e. w ) )
47 simpr23 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) )
48 eleq1 
 |-  ( ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) -> ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) )
49 48 ralimi 
 |-  ( A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) -> A. y e. b ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) )
50 ralbi 
 |-  ( A. y e. b ( ( ( a +no y ) +no c ) e. w <-> ( a +no ( y +no c ) ) e. w ) -> ( A. y e. b ( ( a +no y ) +no c ) e. w <-> A. y e. b ( a +no ( y +no c ) ) e. w ) )
51 47 49 50 3syl 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. y e. b ( ( a +no y ) +no c ) e. w <-> A. y e. b ( a +no ( y +no c ) ) e. w ) )
52 simpr3 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) )
53 eleq1 
 |-  ( ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) -> ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) )
54 53 ralimi 
 |-  ( A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) -> A. z e. c ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) )
55 ralbi 
 |-  ( A. z e. c ( ( ( a +no b ) +no z ) e. w <-> ( a +no ( b +no z ) ) e. w ) -> ( A. z e. c ( ( a +no b ) +no z ) e. w <-> A. z e. c ( a +no ( b +no z ) ) e. w ) )
56 52 54 55 3syl 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( A. z e. c ( ( a +no b ) +no z ) e. w <-> A. z e. c ( a +no ( b +no z ) ) e. w ) )
57 46 51 56 3anbi123d 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) <-> ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) ) )
58 57 rabbidv 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } = { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } )
59 58 inteqd 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } )
60 naddasslem1 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( a +no b ) +no c ) = |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } )
61 60 adantr 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( a +no b ) +no c ) = |^| { w e. On | ( A. x e. a ( ( x +no b ) +no c ) e. w /\ A. y e. b ( ( a +no y ) +no c ) e. w /\ A. z e. c ( ( a +no b ) +no z ) e. w ) } )
62 naddasslem2 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( a +no ( b +no c ) ) = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } )
63 62 adantr 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( a +no ( b +no c ) ) = |^| { w e. On | ( A. x e. a ( x +no ( b +no c ) ) e. w /\ A. y e. b ( a +no ( y +no c ) ) e. w /\ A. z e. c ( a +no ( b +no z ) ) e. w ) } )
64 59 61 63 3eqtr4d 
 |-  ( ( ( a e. On /\ b e. On /\ c e. On ) /\ ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) ) -> ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) )
65 64 ex 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. x e. a A. y e. b A. z e. c ( ( x +no y ) +no z ) = ( x +no ( y +no z ) ) /\ A. x e. a A. y e. b ( ( x +no y ) +no c ) = ( x +no ( y +no c ) ) /\ A. x e. a A. z e. c ( ( x +no b ) +no z ) = ( x +no ( b +no z ) ) ) /\ ( A. x e. a ( ( x +no b ) +no c ) = ( x +no ( b +no c ) ) /\ A. y e. b A. z e. c ( ( a +no y ) +no z ) = ( a +no ( y +no z ) ) /\ A. y e. b ( ( a +no y ) +no c ) = ( a +no ( y +no c ) ) ) /\ A. z e. c ( ( a +no b ) +no z ) = ( a +no ( b +no z ) ) ) -> ( ( a +no b ) +no c ) = ( a +no ( b +no c ) ) ) )
66 4 9 13 17 22 25 28 32 37 41 65 on3ind 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( A +no ( B +no C ) ) )