oaass - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > oaass		Unicode version

Theorem oaass 6763

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

**Assertion**
Ref	Expression
oaass	$/\$ $/\$

Proof of Theorem oaass Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6048	. . . . 5
2		oveq2 6048	. . . . . 6
3	2	oveq2d 6056	. . . . 5
4	1, 3	eqeq12d 2418	. . . 4
5		oveq2 6048	. . . . 5
6		oveq2 6048	. . . . . 6
7	6	oveq2d 6056	. . . . 5
8	5, 7	eqeq12d 2418	. . . 4
9		oveq2 6048	. . . . 5
10		oveq2 6048	. . . . . 6
11	10	oveq2d 6056	. . . . 5
12	9, 11	eqeq12d 2418	. . . 4
13		oveq2 6048	. . . . 5
14		oveq2 6048	. . . . . 6
15	14	oveq2d 6056	. . . . 5
16	13, 15	eqeq12d 2418	. . . 4
17		oacl 6738	. . . . . 6 $/\$
18		oa0 6719	. . . . . 6
19	17, 18	syl 16	. . . . 5 $/\$
20		oa0 6719	. . . . . . 7
21	20	oveq2d 6056	. . . . . 6
22	21	adantl 453	. . . . 5 $/\$
23	19, 22	eqtr4d 2439	. . . 4 $/\$
24		suceq 4606	. . . . . 6
25		oasuc 6727	. . . . . . . 8 $/\$
26	17, 25	sylan 458	. . . . . . 7 $/\$ $/\$
27		oasuc 6727	. . . . . . . . . . 11 $/\$
28	27	oveq2d 6056	. . . . . . . . . 10 $/\$
29	28	adantl 453	. . . . . . . . 9 $/\$ $/\$
30		oacl 6738	. . . . . . . . . 10 $/\$
31		oasuc 6727	. . . . . . . . . 10 $/\$
32	30, 31	sylan2 461	. . . . . . . . 9 $/\$ $/\$
33	29, 32	eqtrd 2436	. . . . . . . 8 $/\$ $/\$
34	33	anassrs 630	. . . . . . 7 $/\$ $/\$
35	26, 34	eqeq12d 2418	. . . . . 6 $/\$ $/\$
36	24, 35	syl5ibr 213	. . . . 5 $/\$ $/\$
37	36	expcom 425	. . . 4 $/\$
38		vex 2919	. . . . . . . . . 10
39		oalim 6735	. . . . . . . . . 10 $/\$ $/\$
40	38, 39	mpanr1 665	. . . . . . . . 9 $/\$
41	17, 40	sylan 458	. . . . . . . 8 $/\$ $/\$
42	41	ancoms 440	. . . . . . 7 $/\$ $/\$
43	42	adantr 452	. . . . . 6 $/\$ $/\$ $/\$
44		oalimcl 6762	. . . . . . . . . . . . 13 $/\$ $/\$
45	38, 44	mpanr1 665	. . . . . . . . . . . 12 $/\$
46	45	ancoms 440	. . . . . . . . . . 11 $/\$
47		ovex 6065	. . . . . . . . . . . 12
48		oalim 6735	. . . . . . . . . . . 12 $/\$ $/\$
49	47, 48	mpanr1 665	. . . . . . . . . . 11 $/\$
50	46, 49	sylan2 461	. . . . . . . . . 10 $/\$ $/\$
51		limelon 4604	. . . . . . . . . . . . . . . . . 18 $/\$
52	38, 51	mpan 652	. . . . . . . . . . . . . . . . 17
53		oacl 6738	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
54	53	ancoms 440	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
55		onelon 4566	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
56	55	ex 424	. . . . . . . . . . . . . . . . . . . . . 22
57	54, 56	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58	57	adantld 454	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
59	58	adantl 453	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
60		0ellim 4603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
61		onelss 4583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
62	20	sseq2d 3336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63	61, 62	sylibrd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
64	63	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
65		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
66	65	sseq2d 3336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
67	66	rspcev 3012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
68	60, 64, 67	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	68	expr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	adantrl 697	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
71	70	adantrr 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
72		oawordex 6759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
73	72	ad2ant2l 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
74		oaord 6749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
75	74	3expb 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
76		eleq1 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
77	75, 76	sylan9bb 681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
78	77	an32s 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
79	78	biimpar 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
80		eqimss2 3361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
81	80	ad3antlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
82	79, 81	jca 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
83	82	anasss 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
84	83	expcom 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
85	84	reximdv2 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
86	85	adantrr 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
87	73, 86	sylbid 207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
88	87	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
89		eloni 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
90		eloni 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
91		ordtri2or 4636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$
92	89, 90, 91	syl2anr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$
93	92	ad2ant2l 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\/$
94	93	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\/$
95	71, 88, 94	mpjaod 371	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
96	95	exp45 598	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
97	96	imp 419	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	97	adantld 454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
99	98	imp32 423	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100		simplrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		onelon 4566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
102	101, 30	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
103	102	exp32 589	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104	103	com12 29	. . . . . . . . . . . . . . . . . . . . . . . . . 26
105	104	imp31 422	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
106	105	adantll 695	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
107	106	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		simpll 731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
109	108	ad2antlr 708	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110		oaword 6751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
111	100, 107, 109, 110	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	111	rexbidva 2683	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	99, 112	mpbid 202	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
114	113	exp32 589	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	59, 114	mpdd 38	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	115	exp32 589	. . . . . . . . . . . . . . . . 17 $/\$
117	52, 116	mpd 15	. . . . . . . . . . . . . . . 16 $/\$
118	117	exp4a 590	. . . . . . . . . . . . . . 15
119	118	imp31 422	. . . . . . . . . . . . . 14 $/\$ $/\$
120	119	ralrimiv 2748	. . . . . . . . . . . . 13 $/\$ $/\$
121		iunss2 4096	. . . . . . . . . . . . 13
122	120, 121	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
123	122	ancoms 440	. . . . . . . . . . 11 $/\$ $/\$
124		oaordi 6748	. . . . . . . . . . . . . . . . . . 19 $/\$
125	124	anim1d 548	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126		oveq2 6048	. . . . . . . . . . . . . . . . . . . 20
127	126	eleq2d 2471	. . . . . . . . . . . . . . . . . . 19
128	127	rspcev 3012	. . . . . . . . . . . . . . . . . 18 $/\$
129	125, 128	syl6 31	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
130	129	exp3a 426	. . . . . . . . . . . . . . . 16 $/\$
131	130	rexlimdv 2789	. . . . . . . . . . . . . . 15 $/\$
132		eliun 4057	. . . . . . . . . . . . . . 15
133		eliun 4057	. . . . . . . . . . . . . . 15
134	131, 132, 133	3imtr4g 262	. . . . . . . . . . . . . 14 $/\$
135	134	ssrdv 3314	. . . . . . . . . . . . 13 $/\$
136	52, 135	sylan 458	. . . . . . . . . . . 12 $/\$
137	136	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
138	123, 137	eqssd 3325	. . . . . . . . . 10 $/\$ $/\$
139	50, 138	eqtrd 2436	. . . . . . . . 9 $/\$ $/\$
140	139	an12s 777	. . . . . . . 8 $/\$ $/\$
141	140	adantr 452	. . . . . . 7 $/\$ $/\$ $/\$
142		iuneq2 4069	. . . . . . . 8
143	142	adantl 453	. . . . . . 7 $/\$ $/\$ $/\$
144	141, 143	eqtr4d 2439	. . . . . 6 $/\$ $/\$ $/\$
145	43, 144	eqtr4d 2439	. . . . 5 $/\$ $/\$ $/\$
146	145	exp31 588	. . . 4 $/\$
147	4, 8, 12, 16, 23, 37, 146	tfinds3 4803	. . 3 $/\$
148	147	com12 29	. 2 $/\$
149	148	3impia 1150	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2666

wrex 2667

cvv 2916

wss 3280

c0 3588

ciun 4053

word 4540

con0 4541

wlim 4542

csuc 4543 (class class class)co 6040

coa 6680

This theorem is referenced by: odi 6781 oaabs 6846 oaabs2 6847

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-recs 6592 df-rdg 6627 df-oadd 6687

W3C validator