Theorem odi 7659

Description: Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of [TakeutiZaring] p. 64. (Contributed by NM, 26-Dec-2004.)

Assertion

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

Proof of Theorem odi

Dummy variables x y z w v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6658	. . . . . 6 |- ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
2	1	oveq2d 6666	. . . . 5 |- ( x = (/) -> ( A .o ( B +o x ) ) = ( A .o ( B +o (/) ) ) )
3		oveq2 6658	. . . . . 6 |- ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
4	3	oveq2d 6666	. . . . 5 |- ( x = (/) -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o (/) ) ) )
5	2, 4	eqeq12d 2637	. . . 4 |- ( x = (/) -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o (/) ) ) = ( ( A .o B ) +o ( A .o (/) ) ) ) )
6		oveq2 6658	. . . . . 6 |- ( x = y -> ( B +o x ) = ( B +o y ) )
7	6	oveq2d 6666	. . . . 5 |- ( x = y -> ( A .o ( B +o x ) ) = ( A .o ( B +o y ) ) )
8		oveq2 6658	. . . . . 6 |- ( x = y -> ( A .o x ) = ( A .o y ) )
9	8	oveq2d 6666	. . . . 5 |- ( x = y -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o y ) ) )
10	7, 9	eqeq12d 2637	. . . 4 |- ( x = y -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) )
11		oveq2 6658	. . . . . 6 |- ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
12	11	oveq2d 6666	. . . . 5 |- ( x = suc y -> ( A .o ( B +o x ) ) = ( A .o ( B +o suc y ) ) )
13		oveq2 6658	. . . . . 6 |- ( x = suc y -> ( A .o x ) = ( A .o suc y ) )
14	13	oveq2d 6666	. . . . 5 |- ( x = suc y -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o suc y ) ) )
15	12, 14	eqeq12d 2637	. . . 4 |- ( x = suc y -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) )
16		oveq2 6658	. . . . . 6 |- ( x = C -> ( B +o x ) = ( B +o C ) )
17	16	oveq2d 6666	. . . . 5 |- ( x = C -> ( A .o ( B +o x ) ) = ( A .o ( B +o C ) ) )
18		oveq2 6658	. . . . . 6 |- ( x = C -> ( A .o x ) = ( A .o C ) )
19	18	oveq2d 6666	. . . . 5 |- ( x = C -> ( ( A .o B ) +o ( A .o x ) ) = ( ( A .o B ) +o ( A .o C ) ) )
20	17, 19	eqeq12d 2637	. . . 4 |- ( x = C -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) )
21		omcl 7616	. . . . . 6 |- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
22		oa0 7596	. . . . . 6 |- ( ( A .o B ) e. On -> ( ( A .o B ) +o (/) ) = ( A .o B ) )
23	21, 22	syl 17	. . . . 5 |- ( ( A e. On /\ B e. On ) -> ( ( A .o B ) +o (/) ) = ( A .o B ) )
24		om0 7597	. . . . . . 7 |- ( A e. On -> ( A .o (/) ) = (/) )
25	24	adantr 481	. . . . . 6 |- ( ( A e. On /\ B e. On ) -> ( A .o (/) ) = (/) )
26	25	oveq2d 6666	. . . . 5 |- ( ( A e. On /\ B e. On ) -> ( ( A .o B ) +o ( A .o (/) ) ) = ( ( A .o B ) +o (/) ) )
27		oa0 7596	. . . . . . 7 |- ( B e. On -> ( B +o (/) ) = B )
28	27	adantl 482	. . . . . 6 |- ( ( A e. On /\ B e. On ) -> ( B +o (/) ) = B )
29	28	oveq2d 6666	. . . . 5 |- ( ( A e. On /\ B e. On ) -> ( A .o ( B +o (/) ) ) = ( A .o B ) )
30	23, 26, 29	3eqtr4rd 2667	. . . 4 |- ( ( A e. On /\ B e. On ) -> ( A .o ( B +o (/) ) ) = ( ( A .o B ) +o ( A .o (/) ) ) )
31		oveq1 6657	. . . . . . . 8 |- ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( ( A .o ( B +o y ) ) +o A ) = ( ( ( A .o B ) +o ( A .o y ) ) +o A ) )
32		oasuc 7604	. . . . . . . . . . . 12 |- ( ( B e. On /\ y e. On ) -> ( B +o suc y ) = suc ( B +o y ) )
33	32	3adant1 1079	. . . . . . . . . . 11 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( B +o suc y ) = suc ( B +o y ) )
34	33	oveq2d 6666	. . . . . . . . . 10 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o ( B +o suc y ) ) = ( A .o suc ( B +o y ) ) )
35		oacl 7615	. . . . . . . . . . . 12 |- ( ( B e. On /\ y e. On ) -> ( B +o y ) e. On )
36		omsuc 7606	. . . . . . . . . . . 12 |- ( ( A e. On /\ ( B +o y ) e. On ) -> ( A .o suc ( B +o y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
37	35, 36	sylan2 491	. . . . . . . . . . 11 |- ( ( A e. On /\ ( B e. On /\ y e. On ) ) -> ( A .o suc ( B +o y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
38	37	3impb 1260	. . . . . . . . . 10 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o suc ( B +o y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
39	34, 38	eqtrd 2656	. . . . . . . . 9 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o ( B +o suc y ) ) = ( ( A .o ( B +o y ) ) +o A ) )
40		omsuc 7606	. . . . . . . . . . . 12 |- ( ( A e. On /\ y e. On ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
41	40	3adant2 1080	. . . . . . . . . . 11 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
42	41	oveq2d 6666	. . . . . . . . . 10 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A .o B ) +o ( A .o suc y ) ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
43		omcl 7616	. . . . . . . . . . . . . . . . 17 |- ( ( A e. On /\ y e. On ) -> ( A .o y ) e. On )
44		oaass 7641	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A .o B ) e. On /\ ( A .o y ) e. On /\ A e. On ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
45	21, 44	syl3an1 1359	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. On /\ B e. On ) /\ ( A .o y ) e. On /\ A e. On ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
46	43, 45	syl3an2 1360	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. On /\ B e. On ) /\ ( A e. On /\ y e. On ) /\ A e. On ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
47	46	3exp 1264	. . . . . . . . . . . . . . 15 |- ( ( A e. On /\ B e. On ) -> ( ( A e. On /\ y e. On ) -> ( A e. On -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) )
48	47	exp4b 632	. . . . . . . . . . . . . 14 |- ( A e. On -> ( B e. On -> ( A e. On -> ( y e. On -> ( A e. On -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) ) ) )
49	48	pm2.43a 54	. . . . . . . . . . . . 13 |- ( A e. On -> ( B e. On -> ( y e. On -> ( A e. On -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) ) )
50	49	com4r 94	. . . . . . . . . . . 12 |- ( A e. On -> ( A e. On -> ( B e. On -> ( y e. On -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) ) )
51	50	pm2.43i 52	. . . . . . . . . . 11 |- ( A e. On -> ( B e. On -> ( y e. On -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) ) ) )
52	51	3imp 1256	. . . . . . . . . 10 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( ( A .o B ) +o ( A .o y ) ) +o A ) = ( ( A .o B ) +o ( ( A .o y ) +o A ) ) )
53	42, 52	eqtr4d 2659	. . . . . . . . 9 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A .o B ) +o ( A .o suc y ) ) = ( ( ( A .o B ) +o ( A .o y ) ) +o A ) )
54	39, 53	eqeq12d 2637	. . . . . . . 8 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) <-> ( ( A .o ( B +o y ) ) +o A ) = ( ( ( A .o B ) +o ( A .o y ) ) +o A ) ) )
55	31, 54	syl5ibr 236	. . . . . . 7 |- ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) )
56	55	3exp 1264	. . . . . 6 |- ( A e. On -> ( B e. On -> ( y e. On -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) ) ) )
57	56	com3r 87	. . . . 5 |- ( y e. On -> ( A e. On -> ( B e. On -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) ) ) )
58	57	impd 447	. . . 4 |- ( y e. On -> ( ( A e. On /\ B e. On ) -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o suc y ) ) = ( ( A .o B ) +o ( A .o suc y ) ) ) ) )
59		vex 3203	. . . . . . . . . . . . . 14 |- x e. _V
60		limelon 5788	. . . . . . . . . . . . . 14 |- ( ( x e. _V /\ Lim x ) -> x e. On )
61	59, 60	mpan 706	. . . . . . . . . . . . 13 |- ( Lim x -> x e. On )
62		oacl 7615	. . . . . . . . . . . . . . 15 |- ( ( B e. On /\ x e. On ) -> ( B +o x ) e. On )
63		om0r 7619	. . . . . . . . . . . . . . 15 |- ( ( B +o x ) e. On -> ( (/) .o ( B +o x ) ) = (/) )
64	62, 63	syl 17	. . . . . . . . . . . . . 14 |- ( ( B e. On /\ x e. On ) -> ( (/) .o ( B +o x ) ) = (/) )
65		om0r 7619	. . . . . . . . . . . . . . . 16 |- ( B e. On -> ( (/) .o B ) = (/) )
66		om0r 7619	. . . . . . . . . . . . . . . 16 |- ( x e. On -> ( (/) .o x ) = (/) )
67	65, 66	oveqan12d 6669	. . . . . . . . . . . . . . 15 |- ( ( B e. On /\ x e. On ) -> ( ( (/) .o B ) +o ( (/) .o x ) ) = ( (/) +o (/) ) )
68		0elon 5778	. . . . . . . . . . . . . . . 16 |- (/) e. On
69		oa0 7596	. . . . . . . . . . . . . . . 16 |- ( (/) e. On -> ( (/) +o (/) ) = (/) )
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( (/) +o (/) ) = (/)
71	67, 70	syl6req 2673	. . . . . . . . . . . . . 14 |- ( ( B e. On /\ x e. On ) -> (/) = ( ( (/) .o B ) +o ( (/) .o x ) ) )
72	64, 71	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( B e. On /\ x e. On ) -> ( (/) .o ( B +o x ) ) = ( ( (/) .o B ) +o ( (/) .o x ) ) )
73	61, 72	sylan2 491	. . . . . . . . . . . 12 |- ( ( B e. On /\ Lim x ) -> ( (/) .o ( B +o x ) ) = ( ( (/) .o B ) +o ( (/) .o x ) ) )
74	73	ancoms 469	. . . . . . . . . . 11 |- ( ( Lim x /\ B e. On ) -> ( (/) .o ( B +o x ) ) = ( ( (/) .o B ) +o ( (/) .o x ) ) )
75		oveq1 6657	. . . . . . . . . . . 12 |- ( A = (/) -> ( A .o ( B +o x ) ) = ( (/) .o ( B +o x ) ) )
76		oveq1 6657	. . . . . . . . . . . . 13 |- ( A = (/) -> ( A .o B ) = ( (/) .o B ) )
77		oveq1 6657	. . . . . . . . . . . . 13 |- ( A = (/) -> ( A .o x ) = ( (/) .o x ) )
78	76, 77	oveq12d 6668	. . . . . . . . . . . 12 |- ( A = (/) -> ( ( A .o B ) +o ( A .o x ) ) = ( ( (/) .o B ) +o ( (/) .o x ) ) )
79	75, 78	eqeq12d 2637	. . . . . . . . . . 11 |- ( A = (/) -> ( ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) <-> ( (/) .o ( B +o x ) ) = ( ( (/) .o B ) +o ( (/) .o x ) ) ) )
80	74, 79	syl5ibr 236	. . . . . . . . . 10 |- ( A = (/) -> ( ( Lim x /\ B e. On ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) )
81	80	expd 452	. . . . . . . . 9 |- ( A = (/) -> ( Lim x -> ( B e. On -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) )
82	81	com3r 87	. . . . . . . 8 |- ( B e. On -> ( A = (/) -> ( Lim x -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) )
83	82	imp 445	. . . . . . 7 |- ( ( B e. On /\ A = (/) ) -> ( Lim x -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) )
84	83	a1dd 50	. . . . . 6 |- ( ( B e. On /\ A = (/) ) -> ( Lim x -> ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) )
85		simplr 792	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> B e. On )
86	62	ancoms 469	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. On /\ B e. On ) -> ( B +o x ) e. On )
87		onelon 5748	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( B +o x ) e. On /\ z e. ( B +o x ) ) -> z e. On )
88	86, 87	sylan 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> z e. On )
89		ontri1 5757	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( B e. On /\ z e. On ) -> ( B C_ z <-> -. z e. B ) )
90		oawordex 7637	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( B e. On /\ z e. On ) -> ( B C_ z <-> E. v e. On ( B +o v ) = z ) )
91	89, 90	bitr3d 270	. . . . . . . . . . . . . . . . . . . 20 |- ( ( B e. On /\ z e. On ) -> ( -. z e. B <-> E. v e. On ( B +o v ) = z ) )
92	85, 88, 91	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( -. z e. B <-> E. v e. On ( B +o v ) = z ) )
93		oaord 7627	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( v e. On /\ x e. On /\ B e. On ) -> ( v e. x <-> ( B +o v ) e. ( B +o x ) ) )
94	93	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( v e. On /\ ( x e. On /\ B e. On ) ) -> ( v e. x <-> ( B +o v ) e. ( B +o x ) ) )
95		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( B +o v ) = z -> ( ( B +o v ) e. ( B +o x ) <-> z e. ( B +o x ) ) )
96	94, 95	sylan9bb 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( v e. On /\ ( x e. On /\ B e. On ) ) /\ ( B +o v ) = z ) -> ( v e. x <-> z e. ( B +o x ) ) )
97		iba 524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( B +o v ) = z -> ( v e. x <-> ( v e. x /\ ( B +o v ) = z ) ) )
98	97	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( v e. On /\ ( x e. On /\ B e. On ) ) /\ ( B +o v ) = z ) -> ( v e. x <-> ( v e. x /\ ( B +o v ) = z ) ) )
99	96, 98	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( v e. On /\ ( x e. On /\ B e. On ) ) /\ ( B +o v ) = z ) -> ( z e. ( B +o x ) <-> ( v e. x /\ ( B +o v ) = z ) ) )
100	99	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( v e. On /\ ( B +o v ) = z ) /\ ( x e. On /\ B e. On ) ) -> ( z e. ( B +o x ) <-> ( v e. x /\ ( B +o v ) = z ) ) )
101	100	biimpcd 239	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. ( B +o x ) -> ( ( ( v e. On /\ ( B +o v ) = z ) /\ ( x e. On /\ B e. On ) ) -> ( v e. x /\ ( B +o v ) = z ) ) )
102	101	exp4c 636	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( B +o x ) -> ( v e. On -> ( ( B +o v ) = z -> ( ( x e. On /\ B e. On ) -> ( v e. x /\ ( B +o v ) = z ) ) ) ) )
103	102	com4r 94	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. On /\ B e. On ) -> ( z e. ( B +o x ) -> ( v e. On -> ( ( B +o v ) = z -> ( v e. x /\ ( B +o v ) = z ) ) ) ) )
104	103	imp 445	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( v e. On -> ( ( B +o v ) = z -> ( v e. x /\ ( B +o v ) = z ) ) ) )
105	104	reximdvai 3015	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( E. v e. On ( B +o v ) = z -> E. v e. On ( v e. x /\ ( B +o v ) = z ) ) )
106	92, 105	sylbid 230	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( -. z e. B -> E. v e. On ( v e. x /\ ( B +o v ) = z ) ) )
107	106	orrd 393	. . . . . . . . . . . . . . . . 17 |- ( ( ( x e. On /\ B e. On ) /\ z e. ( B +o x ) ) -> ( z e. B \/ E. v e. On ( v e. x /\ ( B +o v ) = z ) ) )
108	61, 107	sylanl1 682	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ B e. On ) /\ z e. ( B +o x ) ) -> ( z e. B \/ E. v e. On ( v e. x /\ ( B +o v ) = z ) ) )
109	108	adantlrl 756	. . . . . . . . . . . . . . 15 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ z e. ( B +o x ) ) -> ( z e. B \/ E. v e. On ( v e. x /\ ( B +o v ) = z ) ) )
110	109	adantlr 751	. . . . . . . . . . . . . 14 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) /\ z e. ( B +o x ) ) -> ( z e. B \/ E. v e. On ( v e. x /\ ( B +o v ) = z ) ) )
111		0ellim 5787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( Lim x -> (/) e. x )
112		om00el 7656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( A e. On /\ x e. On ) -> ( (/) e. ( A .o x ) <-> ( (/) e. A /\ (/) e. x ) ) )
113	112	biimprd 238	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A e. On /\ x e. On ) -> ( ( (/) e. A /\ (/) e. x ) -> (/) e. ( A .o x ) ) )
114	111, 113	sylan2i 687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A e. On /\ x e. On ) -> ( ( (/) e. A /\ Lim x ) -> (/) e. ( A .o x ) ) )
115	61, 114	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A e. On /\ Lim x ) -> ( ( (/) e. A /\ Lim x ) -> (/) e. ( A .o x ) ) )
116	115	exp4b 632	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. On -> ( Lim x -> ( (/) e. A -> ( Lim x -> (/) e. ( A .o x ) ) ) ) )
117	116	com4r 94	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Lim x -> ( A e. On -> ( Lim x -> ( (/) e. A -> (/) e. ( A .o x ) ) ) ) )
118	117	pm2.43a 54	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Lim x -> ( A e. On -> ( (/) e. A -> (/) e. ( A .o x ) ) ) )
119	118	imp31 448	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Lim x /\ A e. On ) /\ (/) e. A ) -> (/) e. ( A .o x ) )
120	119	a1d 25	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Lim x /\ A e. On ) /\ (/) e. A ) -> ( z e. B -> (/) e. ( A .o x ) ) )
121	120	adantlrr 757	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( z e. B -> (/) e. ( A .o x ) ) )
122		omordi 7646	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( B e. On /\ A e. On ) /\ (/) e. A ) -> ( z e. B -> ( A .o z ) e. ( A .o B ) ) )
123	122	ancom1s 847	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( z e. B -> ( A .o z ) e. ( A .o B ) ) )
124		onelss 5766	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A .o B ) e. On -> ( ( A .o z ) e. ( A .o B ) -> ( A .o z ) C_ ( A .o B ) ) )
125	22	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A .o B ) e. On -> ( ( A .o z ) C_ ( ( A .o B ) +o (/) ) <-> ( A .o z ) C_ ( A .o B ) ) )
126	124, 125	sylibrd 249	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A .o B ) e. On -> ( ( A .o z ) e. ( A .o B ) -> ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) )
127	21, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. On /\ B e. On ) -> ( ( A .o z ) e. ( A .o B ) -> ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) )
128	127	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( ( A .o z ) e. ( A .o B ) -> ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) )
129	123, 128	syld 47	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( z e. B -> ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) )
130	129	adantll 750	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( z e. B -> ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) )
131	121, 130	jcad 555	. . . . . . . . . . . . . . . . . 18 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( z e. B -> ( (/) e. ( A .o x ) /\ ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) ) )
132		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( w = (/) -> ( ( A .o B ) +o w ) = ( ( A .o B ) +o (/) ) )
133	132	sseq2d 3633	. . . . . . . . . . . . . . . . . . 19 |- ( w = (/) -> ( ( A .o z ) C_ ( ( A .o B ) +o w ) <-> ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) )
134	133	rspcev 3309	. . . . . . . . . . . . . . . . . 18 |- ( ( (/) e. ( A .o x ) /\ ( A .o z ) C_ ( ( A .o B ) +o (/) ) ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) )
135	131, 134	syl6 35	. . . . . . . . . . . . . . . . 17 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( z e. B -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
136	135	adantrr 753	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( z e. B -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
137		omordi 7646	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( x e. On /\ A e. On ) /\ (/) e. A ) -> ( v e. x -> ( A .o v ) e. ( A .o x ) ) )
138	61, 137	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Lim x /\ A e. On ) /\ (/) e. A ) -> ( v e. x -> ( A .o v ) e. ( A .o x ) ) )
139	138	adantrd 484	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Lim x /\ A e. On ) /\ (/) e. A ) -> ( ( v e. x /\ ( B +o v ) = z ) -> ( A .o v ) e. ( A .o x ) ) )
140	139	adantrr 753	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Lim x /\ A e. On ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( ( v e. x /\ ( B +o v ) = z ) -> ( A .o v ) e. ( A .o x ) ) )
141		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = v -> ( B +o y ) = ( B +o v ) )
142	141	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = v -> ( A .o ( B +o y ) ) = ( A .o ( B +o v ) ) )
143		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = v -> ( A .o y ) = ( A .o v ) )
144	143	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = v -> ( ( A .o B ) +o ( A .o y ) ) = ( ( A .o B ) +o ( A .o v ) ) )
145	142, 144	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = v -> ( ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) <-> ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) ) )
146	145	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( v e. x -> ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) ) )
147		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( B +o v ) = z -> ( A .o ( B +o v ) ) = ( A .o z ) )
148		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) -> ( ( A .o ( B +o v ) ) = ( A .o z ) <-> ( ( A .o B ) +o ( A .o v ) ) = ( A .o z ) ) )
149	147, 148	syl5ib 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) -> ( ( B +o v ) = z -> ( ( A .o B ) +o ( A .o v ) ) = ( A .o z ) ) )
150		eqimss2 3658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A .o B ) +o ( A .o v ) ) = ( A .o z ) -> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) )
151	149, 150	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) -> ( ( B +o v ) = z -> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) )
152	151	imim2i 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( v e. x -> ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) ) -> ( v e. x -> ( ( B +o v ) = z -> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) ) )
153	152	impd 447	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( v e. x -> ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) ) -> ( ( v e. x /\ ( B +o v ) = z ) -> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) )
154	146, 153	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( ( v e. x /\ ( B +o v ) = z ) -> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) )
155	154	ad2antll 765	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Lim x /\ A e. On ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( ( v e. x /\ ( B +o v ) = z ) -> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) )
156	140, 155	jcad 555	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( Lim x /\ A e. On ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( ( v e. x /\ ( B +o v ) = z ) -> ( ( A .o v ) e. ( A .o x ) /\ ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) ) )
157		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = ( A .o v ) -> ( ( A .o B ) +o w ) = ( ( A .o B ) +o ( A .o v ) ) )
158	157	sseq2d 3633	. . . . . . . . . . . . . . . . . . . 20 |- ( w = ( A .o v ) -> ( ( A .o z ) C_ ( ( A .o B ) +o w ) <-> ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) )
159	158	rspcev 3309	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A .o v ) e. ( A .o x ) /\ ( A .o z ) C_ ( ( A .o B ) +o ( A .o v ) ) ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) )
160	156, 159	syl6 35	. . . . . . . . . . . . . . . . . 18 |- ( ( ( Lim x /\ A e. On ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( ( v e. x /\ ( B +o v ) = z ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
161	160	rexlimdvw 3034	. . . . . . . . . . . . . . . . 17 |- ( ( ( Lim x /\ A e. On ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( E. v e. On ( v e. x /\ ( B +o v ) = z ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
162	161	adantlrr 757	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( E. v e. On ( v e. x /\ ( B +o v ) = z ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
163	136, 162	jaod 395	. . . . . . . . . . . . . . 15 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( ( z e. B \/ E. v e. On ( v e. x /\ ( B +o v ) = z ) ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
164	163	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) /\ z e. ( B +o x ) ) -> ( ( z e. B \/ E. v e. On ( v e. x /\ ( B +o v ) = z ) ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) ) )
165	110, 164	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) /\ z e. ( B +o x ) ) -> E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) )
166	165	ralrimiva 2966	. . . . . . . . . . . 12 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> A. z e. ( B +o x ) E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) )
167		iunss2 4565	. . . . . . . . . . . 12 |- ( A. z e. ( B +o x ) E. w e. ( A .o x ) ( A .o z ) C_ ( ( A .o B ) +o w ) -> U_ z e. ( B +o x ) ( A .o z ) C_ U_ w e. ( A .o x ) ( ( A .o B ) +o w ) )
168	166, 167	syl 17	. . . . . . . . . . 11 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> U_ z e. ( B +o x ) ( A .o z ) C_ U_ w e. ( A .o x ) ( ( A .o B ) +o w ) )
169		omordlim 7657	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ w e. ( A .o x ) ) -> E. v e. x w e. ( A .o v ) )
170	169	ex 450	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( w e. ( A .o x ) -> E. v e. x w e. ( A .o v ) ) )
171	59, 170	mpanr1 719	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. On /\ Lim x ) -> ( w e. ( A .o x ) -> E. v e. x w e. ( A .o v ) ) )
172	171	ancoms 469	. . . . . . . . . . . . . . . . . 18 |- ( ( Lim x /\ A e. On ) -> ( w e. ( A .o x ) -> E. v e. x w e. ( A .o v ) ) )
173	172	imp 445	. . . . . . . . . . . . . . . . 17 |- ( ( ( Lim x /\ A e. On ) /\ w e. ( A .o x ) ) -> E. v e. x w e. ( A .o v ) )
174	173	adantlrr 757	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ w e. ( A .o x ) ) -> E. v e. x w e. ( A .o v ) )
175	174	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ w e. ( A .o x ) ) -> E. v e. x w e. ( A .o v ) )
176		oaordi 7626	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x e. On /\ B e. On ) -> ( v e. x -> ( B +o v ) e. ( B +o x ) ) )
177	61, 176	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( Lim x /\ B e. On ) -> ( v e. x -> ( B +o v ) e. ( B +o x ) ) )
178	177	imp 445	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Lim x /\ B e. On ) /\ v e. x ) -> ( B +o v ) e. ( B +o x ) )
179	178	adantlrl 756	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ v e. x ) -> ( B +o v ) e. ( B +o x ) )
180	179	a1d 25	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( B +o v ) e. ( B +o x ) ) )
181	180	adantlr 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( B +o v ) e. ( B +o x ) ) )
182		limord 5784	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( Lim x -> Ord x )
183		ordelon 5747	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( Ord x /\ v e. x ) -> v e. On )
184	182, 183	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Lim x /\ v e. x ) -> v e. On )
185		omcl 7616	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A e. On /\ v e. On ) -> ( A .o v ) e. On )
186	185	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( v e. On /\ A e. On ) -> ( A .o v ) e. On )
187	186	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( v e. On /\ ( A e. On /\ B e. On ) ) -> ( A .o v ) e. On )
188	21	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( v e. On /\ ( A e. On /\ B e. On ) ) -> ( A .o B ) e. On )
189		oaordi 7626	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A .o v ) e. On /\ ( A .o B ) e. On ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
190	187, 188, 189	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( v e. On /\ ( A e. On /\ B e. On ) ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
191	184, 190	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( Lim x /\ v e. x ) /\ ( A e. On /\ B e. On ) ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
192	191	an32s 846	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
193	192	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
194	145	rspccva 3308	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) /\ v e. x ) -> ( A .o ( B +o v ) ) = ( ( A .o B ) +o ( A .o v ) ) )
195	194	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) /\ v e. x ) -> ( ( ( A .o B ) +o w ) e. ( A .o ( B +o v ) ) <-> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
196	195	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( ( ( A .o B ) +o w ) e. ( A .o ( B +o v ) ) <-> ( ( A .o B ) +o w ) e. ( ( A .o B ) +o ( A .o v ) ) ) )
197	193, 196	sylibrd 249	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) e. ( A .o ( B +o v ) ) ) )
198		oacl 7615	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( B e. On /\ v e. On ) -> ( B +o v ) e. On )
199	198	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( v e. On /\ B e. On ) -> ( B +o v ) e. On )
200		omcl 7616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( A e. On /\ ( B +o v ) e. On ) -> ( A .o ( B +o v ) ) e. On )
201	199, 200	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A e. On /\ ( v e. On /\ B e. On ) ) -> ( A .o ( B +o v ) ) e. On )
202	201	an12s 843	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( v e. On /\ ( A e. On /\ B e. On ) ) -> ( A .o ( B +o v ) ) e. On )
203	184, 202	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( Lim x /\ v e. x ) /\ ( A e. On /\ B e. On ) ) -> ( A .o ( B +o v ) ) e. On )
204	203	an32s 846	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ v e. x ) -> ( A .o ( B +o v ) ) e. On )
205		onelss 5766	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A .o ( B +o v ) ) e. On -> ( ( ( A .o B ) +o w ) e. ( A .o ( B +o v ) ) -> ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) )
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ v e. x ) -> ( ( ( A .o B ) +o w ) e. ( A .o ( B +o v ) ) -> ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) )
207	206	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( ( ( A .o B ) +o w ) e. ( A .o ( B +o v ) ) -> ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) )
208	197, 207	syld 47	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) )
209	181, 208	jcad 555	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> ( ( B +o v ) e. ( B +o x ) /\ ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) ) )
210		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( z = ( B +o v ) -> ( A .o z ) = ( A .o ( B +o v ) ) )
211	210	sseq2d 3633	. . . . . . . . . . . . . . . . . . 19 |- ( z = ( B +o v ) -> ( ( ( A .o B ) +o w ) C_ ( A .o z ) <-> ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) )
212	211	rspcev 3309	. . . . . . . . . . . . . . . . . 18 |- ( ( ( B +o v ) e. ( B +o x ) /\ ( ( A .o B ) +o w ) C_ ( A .o ( B +o v ) ) ) -> E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) )
213	209, 212	syl6 35	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ v e. x ) -> ( w e. ( A .o v ) -> E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) ) )
214	213	rexlimdva 3031	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) -> ( E. v e. x w e. ( A .o v ) -> E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) ) )
215	214	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ w e. ( A .o x ) ) -> ( E. v e. x w e. ( A .o v ) -> E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) ) )
216	175, 215	mpd 15	. . . . . . . . . . . . . 14 |- ( ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) /\ w e. ( A .o x ) ) -> E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) )
217	216	ralrimiva 2966	. . . . . . . . . . . . 13 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) -> A. w e. ( A .o x ) E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) )
218		iunss2 4565	. . . . . . . . . . . . 13 |- ( A. w e. ( A .o x ) E. z e. ( B +o x ) ( ( A .o B ) +o w ) C_ ( A .o z ) -> U_ w e. ( A .o x ) ( ( A .o B ) +o w ) C_ U_ z e. ( B +o x ) ( A .o z ) )
219	217, 218	syl 17	. . . . . . . . . . . 12 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) -> U_ w e. ( A .o x ) ( ( A .o B ) +o w ) C_ U_ z e. ( B +o x ) ( A .o z ) )
220	219	adantrl 752	. . . . . . . . . . 11 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> U_ w e. ( A .o x ) ( ( A .o B ) +o w ) C_ U_ z e. ( B +o x ) ( A .o z ) )
221	168, 220	eqssd 3620	. . . . . . . . . 10 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> U_ z e. ( B +o x ) ( A .o z ) = U_ w e. ( A .o x ) ( ( A .o B ) +o w ) )
222		oalimcl 7640	. . . . . . . . . . . . . . . 16 |- ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> Lim ( B +o x ) )
223	59, 222	mpanr1 719	. . . . . . . . . . . . . . 15 |- ( ( B e. On /\ Lim x ) -> Lim ( B +o x ) )
224	223	ancoms 469	. . . . . . . . . . . . . 14 |- ( ( Lim x /\ B e. On ) -> Lim ( B +o x ) )
225	224	anim2i 593	. . . . . . . . . . . . 13 |- ( ( A e. On /\ ( Lim x /\ B e. On ) ) -> ( A e. On /\ Lim ( B +o x ) ) )
226	225	an12s 843	. . . . . . . . . . . 12 |- ( ( Lim x /\ ( A e. On /\ B e. On ) ) -> ( A e. On /\ Lim ( B +o x ) ) )
227		ovex 6678	. . . . . . . . . . . . 13 |- ( B +o x ) e. _V
228		omlim 7613	. . . . . . . . . . . . 13 |- ( ( 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 ) )
229	227, 228	mpanr1 719	. . . . . . . . . . . 12 |- ( ( A e. On /\ Lim ( B +o x ) ) -> ( A .o ( B +o x ) ) = U_ z e. ( B +o x ) ( A .o z ) )
230	226, 229	syl 17	. . . . . . . . . . 11 |- ( ( Lim x /\ ( A e. On /\ B e. On ) ) -> ( A .o ( B +o x ) ) = U_ z e. ( B +o x ) ( A .o z ) )
231	230	adantr 481	. . . . . . . . . 10 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( A .o ( B +o x ) ) = U_ z e. ( B +o x ) ( A .o z ) )
232	21	ad2antlr 763	. . . . . . . . . . . 12 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( A .o B ) e. On )
233	59	jctl 564	. . . . . . . . . . . . . . . . 17 |- ( Lim x -> ( x e. _V /\ Lim x ) )
234	233	anim2i 593	. . . . . . . . . . . . . . . 16 |- ( ( A e. On /\ Lim x ) -> ( A e. On /\ ( x e. _V /\ Lim x ) ) )
235	234	ancoms 469	. . . . . . . . . . . . . . 15 |- ( ( Lim x /\ A e. On ) -> ( A e. On /\ ( x e. _V /\ Lim x ) ) )
236		omlimcl 7658	. . . . . . . . . . . . . . 15 |- ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ (/) e. A ) -> Lim ( A .o x ) )
237	235, 236	sylan 488	. . . . . . . . . . . . . 14 |- ( ( ( Lim x /\ A e. On ) /\ (/) e. A ) -> Lim ( A .o x ) )
238	237	adantlrr 757	. . . . . . . . . . . . 13 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> Lim ( A .o x ) )
239		ovex 6678	. . . . . . . . . . . . 13 |- ( A .o x ) e. _V
240	238, 239	jctil 560	. . . . . . . . . . . 12 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( ( A .o x ) e. _V /\ Lim ( A .o x ) ) )
241		oalim 7612	. . . . . . . . . . . 12 |- ( ( ( A .o B ) e. On /\ ( ( A .o x ) e. _V /\ Lim ( A .o x ) ) ) -> ( ( A .o B ) +o ( A .o x ) ) = U_ w e. ( A .o x ) ( ( A .o B ) +o w ) )
242	232, 240, 241	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ (/) e. A ) -> ( ( A .o B ) +o ( A .o x ) ) = U_ w e. ( A .o x ) ( ( A .o B ) +o w ) )
243	242	adantrr 753	. . . . . . . . . 10 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( ( A .o B ) +o ( A .o x ) ) = U_ w e. ( A .o x ) ( ( A .o B ) +o w ) )
244	221, 231, 243	3eqtr4d 2666	. . . . . . . . 9 |- ( ( ( Lim x /\ ( A e. On /\ B e. On ) ) /\ ( (/) e. A /\ A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) )
245	244	exp43 640	. . . . . . . 8 |- ( Lim x -> ( ( A e. On /\ B e. On ) -> ( (/) e. A -> ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) ) )
246	245	com3l 89	. . . . . . 7 |- ( ( A e. On /\ B e. On ) -> ( (/) e. A -> ( Lim x -> ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) ) )
247	246	imp 445	. . . . . 6 |- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( Lim x -> ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) )
248	84, 247	oe0lem 7593	. . . . 5 |- ( ( A e. On /\ B e. On ) -> ( Lim x -> ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) )
249	248	com12 32	. . . 4 |- ( Lim x -> ( ( A e. On /\ B e. On ) -> ( A. y e. x ( A .o ( B +o y ) ) = ( ( A .o B ) +o ( A .o y ) ) -> ( A .o ( B +o x ) ) = ( ( A .o B ) +o ( A .o x ) ) ) ) )
250	5, 10, 15, 20, 30, 58, 249	tfinds3 7064	. . 3 |- ( C e. On -> ( ( A e. On /\ B e. On ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) )
251	250	expdcom 455	. 2 |- ( A e. On -> ( B e. On -> ( C e. On -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) ) ) )
252	251	3imp 1256	1 |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   (/)c0 3915   U_ciun 4520   Ord word 5722   Oncon0 5723   Lim wlim 5724   suc csuc 5725  (class class class)co 6650   +o coa 7557   .o comu 7558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-omul 7565

This theorem is referenced by:  omass  7660  oeeui  7682  oaabs2  7725