oaass - Metamath Proof Explorer

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

Theorem oaass 7128

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 6204	. . . . 5
2		oveq2 6204	. . . . . 6
3	2	oveq2d 6212	. . . . 5
4	1, 3	eqeq12d 2404	. . . 4
5		oveq2 6204	. . . . 5
6		oveq2 6204	. . . . . 6
7	6	oveq2d 6212	. . . . 5
8	5, 7	eqeq12d 2404	. . . 4
9		oveq2 6204	. . . . 5
10		oveq2 6204	. . . . . 6
11	10	oveq2d 6212	. . . . 5
12	9, 11	eqeq12d 2404	. . . 4
13		oveq2 6204	. . . . 5
14		oveq2 6204	. . . . . 6
15	14	oveq2d 6212	. . . . 5
16	13, 15	eqeq12d 2404	. . . 4
17		oacl 7103	. . . . . 6 $/\$
18		oa0 7084	. . . . . 6
19	17, 18	syl 16	. . . . 5 $/\$
20		oa0 7084	. . . . . . 7
21	20	oveq2d 6212	. . . . . 6
22	21	adantl 464	. . . . 5 $/\$
23	19, 22	eqtr4d 2426	. . . 4 $/\$
24		suceq 4857	. . . . . 6
25		oasuc 7092	. . . . . . . 8 $/\$
26	17, 25	sylan 469	. . . . . . 7 $/\$ $/\$
27		oasuc 7092	. . . . . . . . . . 11 $/\$
28	27	oveq2d 6212	. . . . . . . . . 10 $/\$
29	28	adantl 464	. . . . . . . . 9 $/\$ $/\$
30		oacl 7103	. . . . . . . . . 10 $/\$
31		oasuc 7092	. . . . . . . . . 10 $/\$
32	30, 31	sylan2 472	. . . . . . . . 9 $/\$ $/\$
33	29, 32	eqtrd 2423	. . . . . . . 8 $/\$ $/\$
34	33	anassrs 646	. . . . . . 7 $/\$ $/\$
35	26, 34	eqeq12d 2404	. . . . . 6 $/\$ $/\$
36	24, 35	syl5ibr 221	. . . . 5 $/\$ $/\$
37	36	expcom 433	. . . 4 $/\$
38		vex 3037	. . . . . . . . . 10
39		oalim 7100	. . . . . . . . . 10 $/\$ $/\$
40	38, 39	mpanr1 681	. . . . . . . . 9 $/\$
41	17, 40	sylan 469	. . . . . . . 8 $/\$ $/\$
42	41	ancoms 451	. . . . . . 7 $/\$ $/\$
43	42	adantr 463	. . . . . 6 $/\$ $/\$ $/\$
44		oalimcl 7127	. . . . . . . . . . . . 13 $/\$ $/\$
45	38, 44	mpanr1 681	. . . . . . . . . . . 12 $/\$
46	45	ancoms 451	. . . . . . . . . . 11 $/\$
47		ovex 6224	. . . . . . . . . . . 12
48		oalim 7100	. . . . . . . . . . . 12 $/\$ $/\$
49	47, 48	mpanr1 681	. . . . . . . . . . 11 $/\$
50	46, 49	sylan2 472	. . . . . . . . . 10 $/\$ $/\$
51		limelon 4855	. . . . . . . . . . . . . . . . . 18 $/\$
52	38, 51	mpan 668	. . . . . . . . . . . . . . . . 17
53		oacl 7103	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
54	53	ancoms 451	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
55		onelon 4817	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
56	55	ex 432	. . . . . . . . . . . . . . . . . . . . . 22
57	54, 56	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
58	57	adantld 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
59	58	adantl 464	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
60		0ellim 4854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
61		onelss 4834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
62	20	sseq2d 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63	61, 62	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
64	63	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
65		oveq2 6204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
66	65	sseq2d 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
67	66	rspcev 3135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
68	60, 64, 67	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	68	expr 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	adantrl 713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
71	70	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
72		oawordex 7124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
73	72	ad2ant2l 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
74		oaord 7114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
75	74	3expb 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
76		eleq1 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
77	75, 76	sylan9bb 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
78	77	an32s 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
79	78	biimpar 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
80		eqimss2 3470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
81	80	ad3antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
82	79, 81	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
83	82	anasss 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
84	83	expcom 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
85	84	reximdv2 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
86	85	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
87	73, 86	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
88	87	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
89		eloni 4802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
90		eloni 4802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
91		ordtri2or 4887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$
92	89, 90, 91	syl2anr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$
93	92	ad2ant2l 743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\/$
94	93	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\/$
95	71, 88, 94	mpjaod 379	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
96	95	exp45 612	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
97	96	imp 427	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
98	97	adantld 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
99	98	imp32 431	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100		simplrr 760	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101		onelon 4817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
102	101, 30	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
103	102	exp32 603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
104	103	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . 26
105	104	imp31 430	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
106	105	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
107	106	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		simpll 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
109	108	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110		oaword 7116	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
111	100, 107, 109, 110	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	111	rexbidva 2890	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
113	99, 112	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
114	113	exp32 603	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	59, 114	mpdd 40	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
116	115	exp32 603	. . . . . . . . . . . . . . . . 17 $/\$
117	52, 116	mpd 15	. . . . . . . . . . . . . . . 16 $/\$
118	117	exp4a 604	. . . . . . . . . . . . . . 15
119	118	imp31 430	. . . . . . . . . . . . . 14 $/\$ $/\$
120	119	ralrimiv 2794	. . . . . . . . . . . . 13 $/\$ $/\$
121		iunss2 4288	. . . . . . . . . . . . 13
122	120, 121	syl 16	. . . . . . . . . . . 12 $/\$ $/\$
123	122	ancoms 451	. . . . . . . . . . 11 $/\$ $/\$
124		oaordi 7113	. . . . . . . . . . . . . . . . . . 19 $/\$
125	124	anim1d 562	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
126		oveq2 6204	. . . . . . . . . . . . . . . . . . . 20
127	126	eleq2d 2452	. . . . . . . . . . . . . . . . . . 19
128	127	rspcev 3135	. . . . . . . . . . . . . . . . . 18 $/\$
129	125, 128	syl6 33	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
130	129	expd 434	. . . . . . . . . . . . . . . 16 $/\$
131	130	rexlimdv 2872	. . . . . . . . . . . . . . 15 $/\$
132		eliun 4248	. . . . . . . . . . . . . . 15
133		eliun 4248	. . . . . . . . . . . . . . 15
134	131, 132, 133	3imtr4g 270	. . . . . . . . . . . . . 14 $/\$
135	134	ssrdv 3423	. . . . . . . . . . . . 13 $/\$
136	52, 135	sylan 469	. . . . . . . . . . . 12 $/\$
137	136	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
138	123, 137	eqssd 3434	. . . . . . . . . 10 $/\$ $/\$
139	50, 138	eqtrd 2423	. . . . . . . . 9 $/\$ $/\$
140	139	an12s 799	. . . . . . . 8 $/\$ $/\$
141	140	adantr 463	. . . . . . 7 $/\$ $/\$ $/\$
142		iuneq2 4260	. . . . . . . 8
143	142	adantl 464	. . . . . . 7 $/\$ $/\$ $/\$
144	141, 143	eqtr4d 2426	. . . . . 6 $/\$ $/\$ $/\$
145	43, 144	eqtr4d 2426	. . . . 5 $/\$ $/\$ $/\$
146	145	exp31 602	. . . 4 $/\$
147	4, 8, 12, 16, 23, 37, 146	tfinds3 6598	. . 3 $/\$
148	147	com12 31	. 2 $/\$
149	148	3impia 1191	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wral 2732

wrex 2733

cvv 3034

wss 3389

c0 3711

ciun 4243

word 4791

con0 4792

wlim 4793

csuc 4794 (class class class)co 6196

coa 7045

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-recs 6960 df-rdg 6994 df-oadd 7052

This theorem is referenced by: odi 7146 oaabs 7211 oaabs2 7212

W3C validator