Metamath Proof Explorer

Theorem oaass

Description: Ordinal addition is associative. Theorem 25 of Suppes p. 211. Theorem 4.2 of Schloeder p. 11. (Contributed by NM, 10-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o (/) ) )
2 oveq2 
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
3 2 oveq2d 
 |-  ( x = (/) -> ( A +o ( B +o x ) ) = ( A +o ( B +o (/) ) ) )
4 1 3 eqeq12d 
 |-  ( x = (/) -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o (/) ) = ( A +o ( B +o (/) ) ) ) )
5 oveq2 
 |-  ( x = y -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o y ) )
6 oveq2 
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
7 6 oveq2d 
 |-  ( x = y -> ( A +o ( B +o x ) ) = ( A +o ( B +o y ) ) )
8 5 7 eqeq12d 
 |-  ( x = y -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) ) )
9 oveq2 
 |-  ( x = suc y -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o suc y ) )
10 oveq2 
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
11 10 oveq2d 
 |-  ( x = suc y -> ( A +o ( B +o x ) ) = ( A +o ( B +o suc y ) ) )
12 9 11 eqeq12d 
 |-  ( x = suc y -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) ) )
13 oveq2 
 |-  ( x = C -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o C ) )
14 oveq2 
 |-  ( x = C -> ( B +o x ) = ( B +o C ) )
15 14 oveq2d 
 |-  ( x = C -> ( A +o ( B +o x ) ) = ( A +o ( B +o C ) ) )
16 13 15 eqeq12d 
 |-  ( x = C -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) )
17 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
18 oa0 
 |-  ( ( A +o B ) e. On -> ( ( A +o B ) +o (/) ) = ( A +o B ) )
19 17 18 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) +o (/) ) = ( A +o B ) )
20 oa0 
 |-  ( B e. On -> ( B +o (/) ) = B )
21 20 oveq2d 
 |-  ( B e. On -> ( A +o ( B +o (/) ) ) = ( A +o B ) )
22 21 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o ( B +o (/) ) ) = ( A +o B ) )
23 19 22 eqtr4d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) +o (/) ) = ( A +o ( B +o (/) ) ) )
24 suceq 
 |-  ( ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> suc ( ( A +o B ) +o y ) = suc ( A +o ( B +o y ) ) )
25 oasuc 
 |-  ( ( ( A +o B ) e. On /\ y e. On ) -> ( ( A +o B ) +o suc y ) = suc ( ( A +o B ) +o y ) )
26 17 25 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( A +o B ) +o suc y ) = suc ( ( A +o B ) +o y ) )
27 oasuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B +o suc y ) = suc ( B +o y ) )
28 27 oveq2d 
 |-  ( ( B e. On /\ y e. On ) -> ( A +o ( B +o suc y ) ) = ( A +o suc ( B +o y ) ) )
29 28 adantl 
 |-  ( ( A e. On /\ ( B e. On /\ y e. On ) ) -> ( A +o ( B +o suc y ) ) = ( A +o suc ( B +o y ) ) )
30 oacl 
 |-  ( ( B e. On /\ y e. On ) -> ( B +o y ) e. On )
31 oasuc 
 |-  ( ( A e. On /\ ( B +o y ) e. On ) -> ( A +o suc ( B +o y ) ) = suc ( A +o ( B +o y ) ) )
32 30 31 sylan2 
 |-  ( ( A e. On /\ ( B e. On /\ y e. On ) ) -> ( A +o suc ( B +o y ) ) = suc ( A +o ( B +o y ) ) )
33 29 32 eqtrd 
 |-  ( ( A e. On /\ ( B e. On /\ y e. On ) ) -> ( A +o ( B +o suc y ) ) = suc ( A +o ( B +o y ) ) )
34 33 anassrs 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( A +o ( B +o suc y ) ) = suc ( A +o ( B +o y ) ) )
35 26 34 eqeq12d 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) <-> suc ( ( A +o B ) +o y ) = suc ( A +o ( B +o y ) ) ) )
36 24 35 imbitrrid 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) ) )
37 36 expcom 
 |-  ( y e. On -> ( ( A e. On /\ B e. On ) -> ( ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) ) ) )
38 iuneq2 
 |-  ( A. y e. x ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> U_ y e. x ( ( A +o B ) +o y ) = U_ y e. x ( A +o ( B +o y ) ) )
39 38 adantl 
 |-  ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) ) -> U_ y e. x ( ( A +o B ) +o y ) = U_ y e. x ( A +o ( B +o y ) ) )
40 vex 
 |-  x e. _V
41 oalim 
 |-  ( ( ( A +o B ) e. On /\ ( x e. _V /\ Lim x ) ) -> ( ( A +o B ) +o x ) = U_ y e. x ( ( A +o B ) +o y ) )
42 40 41 mpanr1 
 |-  ( ( ( A +o B ) e. On /\ Lim x ) -> ( ( A +o B ) +o x ) = U_ y e. x ( ( A +o B ) +o y ) )
43 17 42 sylan 
 |-  ( ( ( A e. On /\ B e. On ) /\ Lim x ) -> ( ( A +o B ) +o x ) = U_ y e. x ( ( A +o B ) +o y ) )
44 43 ancoms 
 |-  ( ( Lim x /\ ( A e. On /\ B e. On ) ) -> ( ( A +o B ) +o x ) = U_ y e. x ( ( A +o B ) +o y ) )
45 44 adantr 
 |-  ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) ) -> ( ( A +o B ) +o x ) = U_ y e. x ( ( A +o B ) +o y ) )
46 oalimcl 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> Lim ( B +o x ) )
47 40 46 mpanr1 
 |-  ( ( B e. On /\ Lim x ) -> Lim ( B +o x ) )
48 47 ancoms 
 |-  ( ( Lim x /\ B e. On ) -> Lim ( B +o x ) )
49 ovex 
 |-  ( B +o x ) e. _V
50 oalim 
 |-  ( ( A e. On /\ ( ( B +o x ) e. _V /\ Lim ( B +o x ) ) ) -> ( A +o ( B +o x ) ) = U_ z e. ( B +o x ) ( A +o z ) )
51 49 50 mpanr1 
 |-  ( ( A e. On /\ Lim ( B +o x ) ) -> ( A +o ( B +o x ) ) = U_ z e. ( B +o x ) ( A +o z ) )
52 48 51 sylan2 
 |-  ( ( A e. On /\ ( Lim x /\ B e. On ) ) -> ( A +o ( B +o x ) ) = U_ z e. ( B +o x ) ( A +o z ) )
53 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
54 40 53 mpan 
 |-  ( Lim x -> x e. On )
55 oacl 
 |-  ( ( B e. On /\ x e. On ) -> ( B +o x ) e. On )
56 55 ancoms 
 |-  ( ( x e. On /\ B e. On ) -> ( B +o x ) e. On )
57 onelon 
 |-  ( ( ( B +o x ) e. On /\ z e. ( B +o x ) ) -> z e. On )
58 57 ex 
 |-  ( ( B +o x ) e. On -> ( z e. ( B +o x ) -> z e. On ) )
59 56 58 syl 
 |-  ( ( x e. On /\ B e. On ) -> ( z e. ( B +o x ) -> z e. On ) )
60 59 adantld 
 |-  ( ( x e. On /\ B e. On ) -> ( ( A e. On /\ z e. ( B +o x ) ) -> z e. On ) )
61 60 adantl 
 |-  ( ( Lim x /\ ( x e. On /\ B e. On ) ) -> ( ( A e. On /\ z e. ( B +o x ) ) -> z e. On ) )
62 0ellim 
 |-  ( Lim x -> (/) e. x )
63 onelss 
 |-  ( B e. On -> ( z e. B -> z C_ B ) )
64 20 sseq2d 
 |-  ( B e. On -> ( z C_ ( B +o (/) ) <-> z C_ B ) )
65 63 64 sylibrd 
 |-  ( B e. On -> ( z e. B -> z C_ ( B +o (/) ) ) )
66 65 imp 
 |-  ( ( B e. On /\ z e. B ) -> z C_ ( B +o (/) ) )
67 oveq2 
 |-  ( y = (/) -> ( B +o y ) = ( B +o (/) ) )
68 67 sseq2d 
 |-  ( y = (/) -> ( z C_ ( B +o y ) <-> z C_ ( B +o (/) ) ) )
69 68 rspcev 
 |-  ( ( (/) e. x /\ z C_ ( B +o (/) ) ) -> E. y e. x z C_ ( B +o y ) )
70 62 66 69 syl2an 
 |-  ( ( Lim x /\ ( B e. On /\ z e. B ) ) -> E. y e. x z C_ ( B +o y ) )
71 70 expr 
 |-  ( ( Lim x /\ B e. On ) -> ( z e. B -> E. y e. x z C_ ( B +o y ) ) )
72 71 adantrl 
 |-  ( ( Lim x /\ ( x e. On /\ B e. On ) ) -> ( z e. B -> E. y e. x z C_ ( B +o y ) ) )
73 72 adantrr 
 |-  ( ( Lim x /\ ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) ) -> ( z e. B -> E. y e. x z C_ ( B +o y ) ) )
74 oawordex 
 |-  ( ( B e. On /\ z e. On ) -> ( B C_ z <-> E. y e. On ( B +o y ) = z ) )
75 74 ad2ant2l 
 |-  ( ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) -> ( B C_ z <-> E. y e. On ( B +o y ) = z ) )
76 oaord 
 |-  ( ( y e. On /\ x e. On /\ B e. On ) -> ( y e. x <-> ( B +o y ) e. ( B +o x ) ) )
77 76 3expb 
 |-  ( ( y e. On /\ ( x e. On /\ B e. On ) ) -> ( y e. x <-> ( B +o y ) e. ( B +o x ) ) )
78 eleq1 
 |-  ( ( B +o y ) = z -> ( ( B +o y ) e. ( B +o x ) <-> z e. ( B +o x ) ) )
79 77 78 sylan9bb 
 |-  ( ( ( y e. On /\ ( x e. On /\ B e. On ) ) /\ ( B +o y ) = z ) -> ( y e. x <-> z e. ( B +o x ) ) )
80 79 an32s 
 |-  ( ( ( y e. On /\ ( B +o y ) = z ) /\ ( x e. On /\ B e. On ) ) -> ( y e. x <-> z e. ( B +o x ) ) )
81 80 biimpar 
 |-  ( ( ( ( y e. On /\ ( B +o y ) = z ) /\ ( x e. On /\ B e. On ) ) /\ z e. ( B +o x ) ) -> y e. x )
82 eqimss2 
 |-  ( ( B +o y ) = z -> z C_ ( B +o y ) )
83 82 ad3antlr 
 |-  ( ( ( ( y e. On /\ ( B +o y ) = z ) /\ ( x e. On /\ B e. On ) ) /\ z e. ( B +o x ) ) -> z C_ ( B +o y ) )
84 81 83 jca 
 |-  ( ( ( ( y e. On /\ ( B +o y ) = z ) /\ ( x e. On /\ B e. On ) ) /\ z e. ( B +o x ) ) -> ( y e. x /\ z C_ ( B +o y ) ) )
85 84 anasss 
 |-  ( ( ( y e. On /\ ( B +o y ) = z ) /\ ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) ) -> ( y e. x /\ z C_ ( B +o y ) ) )
86 85 expcom 
 |-  ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( ( y e. On /\ ( B +o y ) = z ) -> ( y e. x /\ z C_ ( B +o y ) ) ) )
87 86 reximdv2 
 |-  ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( E. y e. On ( B +o y ) = z -> E. y e. x z C_ ( B +o y ) ) )
88 87 adantrr 
 |-  ( ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) -> ( E. y e. On ( B +o y ) = z -> E. y e. x z C_ ( B +o y ) ) )
89 75 88 sylbid 
 |-  ( ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) -> ( B C_ z -> E. y e. x z C_ ( B +o y ) ) )
90 89 adantl 
 |-  ( ( Lim x /\ ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) ) -> ( B C_ z -> E. y e. x z C_ ( B +o y ) ) )
91 eloni 
 |-  ( z e. On -> Ord z )
92 eloni 
 |-  ( B e. On -> Ord B )
93 ordtri2or 
 |-  ( ( Ord z /\ Ord B ) -> ( z e. B \/ B C_ z ) )
94 91 92 93 syl2anr 
 |-  ( ( B e. On /\ z e. On ) -> ( z e. B \/ B C_ z ) )
95 94 ad2ant2l 
 |-  ( ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) -> ( z e. B \/ B C_ z ) )
96 95 adantl 
 |-  ( ( Lim x /\ ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) ) -> ( z e. B \/ B C_ z ) )
97 73 90 96 mpjaod 
 |-  ( ( Lim x /\ ( ( x e. On /\ B e. On ) /\ ( z e. ( B +o x ) /\ z e. On ) ) ) -> E. y e. x z C_ ( B +o y ) )
98 97 exp45 
 |-  ( Lim x -> ( ( x e. On /\ B e. On ) -> ( z e. ( B +o x ) -> ( z e. On -> E. y e. x z C_ ( B +o y ) ) ) ) )
99 98 imp 
 |-  ( ( Lim x /\ ( x e. On /\ B e. On ) ) -> ( z e. ( B +o x ) -> ( z e. On -> E. y e. x z C_ ( B +o y ) ) ) )
100 99 adantld 
 |-  ( ( Lim x /\ ( x e. On /\ B e. On ) ) -> ( ( A e. On /\ z e. ( B +o x ) ) -> ( z e. On -> E. y e. x z C_ ( B +o y ) ) ) )
101 100 imp32 
 |-  ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) -> E. y e. x z C_ ( B +o y ) )
102 simplrr 
 |-  ( ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) /\ y e. x ) -> z e. On )
103 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
104 103 30 sylan2 
 |-  ( ( B e. On /\ ( x e. On /\ y e. x ) ) -> ( B +o y ) e. On )
105 104 exp32 
 |-  ( B e. On -> ( x e. On -> ( y e. x -> ( B +o y ) e. On ) ) )
106 105 com12 
 |-  ( x e. On -> ( B e. On -> ( y e. x -> ( B +o y ) e. On ) ) )
107 106 imp31 
 |-  ( ( ( x e. On /\ B e. On ) /\ y e. x ) -> ( B +o y ) e. On )
108 107 ad4ant24 
 |-  ( ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) /\ y e. x ) -> ( B +o y ) e. On )
109 simpll 
 |-  ( ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) -> A e. On )
110 109 ad2antlr 
 |-  ( ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) /\ y e. x ) -> A e. On )
111 oaword 
 |-  ( ( z e. On /\ ( B +o y ) e. On /\ A e. On ) -> ( z C_ ( B +o y ) <-> ( A +o z ) C_ ( A +o ( B +o y ) ) ) )
112 102 108 110 111 syl3anc 
 |-  ( ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) /\ y e. x ) -> ( z C_ ( B +o y ) <-> ( A +o z ) C_ ( A +o ( B +o y ) ) ) )
113 112 rexbidva 
 |-  ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) -> ( E. y e. x z C_ ( B +o y ) <-> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) )
114 101 113 mpbid 
 |-  ( ( ( Lim x /\ ( x e. On /\ B e. On ) ) /\ ( ( A e. On /\ z e. ( B +o x ) ) /\ z e. On ) ) -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) )
115 114 exp32 
 |-  ( ( Lim x /\ ( x e. On /\ B e. On ) ) -> ( ( A e. On /\ z e. ( B +o x ) ) -> ( z e. On -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) ) )
116 61 115 mpdd 
 |-  ( ( Lim x /\ ( x e. On /\ B e. On ) ) -> ( ( A e. On /\ z e. ( B +o x ) ) -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) )
117 116 exp32 
 |-  ( Lim x -> ( x e. On -> ( B e. On -> ( ( A e. On /\ z e. ( B +o x ) ) -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) ) ) )
118 54 117 mpd 
 |-  ( Lim x -> ( B e. On -> ( ( A e. On /\ z e. ( B +o x ) ) -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) ) )
119 118 exp4a 
 |-  ( Lim x -> ( B e. On -> ( A e. On -> ( z e. ( B +o x ) -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) ) ) )
120 119 imp31 
 |-  ( ( ( Lim x /\ B e. On ) /\ A e. On ) -> ( z e. ( B +o x ) -> E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) ) )
121 120 ralrimiv 
 |-  ( ( ( Lim x /\ B e. On ) /\ A e. On ) -> A. z e. ( B +o x ) E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) )
122 iunss2 
 |-  ( A. z e. ( B +o x ) E. y e. x ( A +o z ) C_ ( A +o ( B +o y ) ) -> U_ z e. ( B +o x ) ( A +o z ) C_ U_ y e. x ( A +o ( B +o y ) ) )
123 121 122 syl 
 |-  ( ( ( Lim x /\ B e. On ) /\ A e. On ) -> U_ z e. ( B +o x ) ( A +o z ) C_ U_ y e. x ( A +o ( B +o y ) ) )
124 123 ancoms 
 |-  ( ( A e. On /\ ( Lim x /\ B e. On ) ) -> U_ z e. ( B +o x ) ( A +o z ) C_ U_ y e. x ( A +o ( B +o y ) ) )
125 oaordi 
 |-  ( ( x e. On /\ B e. On ) -> ( y e. x -> ( B +o y ) e. ( B +o x ) ) )
126 125 anim1d 
 |-  ( ( x e. On /\ B e. On ) -> ( ( y e. x /\ w e. ( A +o ( B +o y ) ) ) -> ( ( B +o y ) e. ( B +o x ) /\ w e. ( A +o ( B +o y ) ) ) ) )
127 oveq2 
 |-  ( z = ( B +o y ) -> ( A +o z ) = ( A +o ( B +o y ) ) )
128 127 eleq2d 
 |-  ( z = ( B +o y ) -> ( w e. ( A +o z ) <-> w e. ( A +o ( B +o y ) ) ) )
129 128 rspcev 
 |-  ( ( ( B +o y ) e. ( B +o x ) /\ w e. ( A +o ( B +o y ) ) ) -> E. z e. ( B +o x ) w e. ( A +o z ) )
130 126 129 syl6 
 |-  ( ( x e. On /\ B e. On ) -> ( ( y e. x /\ w e. ( A +o ( B +o y ) ) ) -> E. z e. ( B +o x ) w e. ( A +o z ) ) )
131 130 expd 
 |-  ( ( x e. On /\ B e. On ) -> ( y e. x -> ( w e. ( A +o ( B +o y ) ) -> E. z e. ( B +o x ) w e. ( A +o z ) ) ) )
132 131 rexlimdv 
 |-  ( ( x e. On /\ B e. On ) -> ( E. y e. x w e. ( A +o ( B +o y ) ) -> E. z e. ( B +o x ) w e. ( A +o z ) ) )
133 eliun 
 |-  ( w e. U_ y e. x ( A +o ( B +o y ) ) <-> E. y e. x w e. ( A +o ( B +o y ) ) )
134 eliun 
 |-  ( w e. U_ z e. ( B +o x ) ( A +o z ) <-> E. z e. ( B +o x ) w e. ( A +o z ) )
135 132 133 134 3imtr4g 
 |-  ( ( x e. On /\ B e. On ) -> ( w e. U_ y e. x ( A +o ( B +o y ) ) -> w e. U_ z e. ( B +o x ) ( A +o z ) ) )
136 135 ssrdv 
 |-  ( ( x e. On /\ B e. On ) -> U_ y e. x ( A +o ( B +o y ) ) C_ U_ z e. ( B +o x ) ( A +o z ) )
137 54 136 sylan 
 |-  ( ( Lim x /\ B e. On ) -> U_ y e. x ( A +o ( B +o y ) ) C_ U_ z e. ( B +o x ) ( A +o z ) )
138 137 adantl 
 |-  ( ( A e. On /\ ( Lim x /\ B e. On ) ) -> U_ y e. x ( A +o ( B +o y ) ) C_ U_ z e. ( B +o x ) ( A +o z ) )
139 124 138 eqssd 
 |-  ( ( A e. On /\ ( Lim x /\ B e. On ) ) -> U_ z e. ( B +o x ) ( A +o z ) = U_ y e. x ( A +o ( B +o y ) ) )
140 52 139 eqtrd 
 |-  ( ( A e. On /\ ( Lim x /\ B e. On ) ) -> ( A +o ( B +o x ) ) = U_ y e. x ( A +o ( B +o y ) ) )
141 140 an12s 
 |-  ( ( Lim x /\ ( A e. On /\ B e. On ) ) -> ( A +o ( B +o x ) ) = U_ y e. x ( A +o ( B +o y ) ) )
142 141 adantr 
 |-  ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) ) -> ( A +o ( B +o x ) ) = U_ y e. x ( A +o ( B +o y ) ) )
143 39 45 142 3eqtr4d 
 |-  ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) ) -> ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) )
144 143 exp31 
 |-  ( Lim x -> ( ( A e. On /\ B e. On ) -> ( A. y e. x ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) ) ) )
145 4 8 12 16 23 37 144 tfinds3 
 |-  ( C e. On -> ( ( A e. On /\ B e. On ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) )
146 145 com12 
 |-  ( ( A e. On /\ B e. On ) -> ( C e. On -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) )
147 146 3impia 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )