Metamath Proof Explorer


Theorem oaass

Description: Ordinal addition is associative. Theorem 25 of Suppes p. 211. (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 syl5ibr
 |-  ( ( ( 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 ) ) )