Theorem oaass 3163

Description: Ordinal addition is associative. Theorem 25 of [Suppes] p. 211.

Assertion

Ref	Expression
oaass	⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → ((A +o B) +o C) = (A +o (B +o C)))

Proof of Theorem oaass

Step	Hyp	Ref	Expression
1		opreq2 3007	. . . . . 6 ⊢ (x = ∅ → ((A +o B) +o x) = ((A +o B) +o ∅))
2		opreq2 3007	. . . . . . 7 ⊢ (x = ∅ → (B +o x) = (B +o ∅))
3	2	opreq2d 3013	. . . . . 6 ⊢ (x = ∅ → (A +o (B +o x)) = (A +o (B +o ∅)))
4	1, 3	cleq12d 1115	. . . . 5 ⊢ (x = ∅ → (((A +o B) +o x) = (A +o (B +o x)) ↔ ((A +o B) +o ∅) = (A +o (B +o ∅))))
5		opreq2 3007	. . . . . 6 ⊢ (x = y → ((A +o B) +o x) = ((A +o B) +o y))
6		opreq2 3007	. . . . . . 7 ⊢ (x = y → (B +o x) = (B +o y))
7	6	opreq2d 3013	. . . . . 6 ⊢ (x = y → (A +o (B +o x)) = (A +o (B +o y)))
8	5, 7	cleq12d 1115	. . . . 5 ⊢ (x = y → (((A +o B) +o x) = (A +o (B +o x)) ↔ ((A +o B) +o y) = (A +o (B +o y))))
9		opreq2 3007	. . . . . 6 ⊢ (x = suc y → ((A +o B) +o x) = ((A +o B) +o suc y))
10		opreq2 3007	. . . . . . 7 ⊢ (x = suc y → (B +o x) = (B +o suc y))
11	10	opreq2d 3013	. . . . . 6 ⊢ (x = suc y → (A +o (B +o x)) = (A +o (B +o suc y)))
12	9, 11	cleq12d 1115	. . . . 5 ⊢ (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		opreq2 3007	. . . . . 6 ⊢ (x = C → ((A +o B) +o x) = ((A +o B) +o C))
14		opreq2 3007	. . . . . . 7 ⊢ (x = C → (B +o x) = (B +o C))
15	14	opreq2d 3013	. . . . . 6 ⊢ (x = C → (A +o (B +o x)) = (A +o (B +o C)))
16	13, 15	cleq12d 1115	. . . . 5 ⊢ (x = C → (((A +o B) +o x) = (A +o (B +o x)) ↔ ((A +o B) +o C) = (A +o (B +o C))))
17		oacl 3138	. . . . . . 7 ⊢ ((A ∈ On ∧ B ∈ On) → (A +o B) ∈ On)
18		oa0 3124	. . . . . . 7 ⊢ ((A +o B) ∈ On → ((A +o B) +o ∅) = (A +o B))
19	17, 18	syl 12	. . . . . 6 ⊢ ((A ∈ On ∧ B ∈ On) → ((A +o B) +o ∅) = (A +o B))
20		oa0 3124	. . . . . . . 8 ⊢ (B ∈ On → (B +o ∅) = B)
21	20	opreq2d 3013	. . . . . . 7 ⊢ (B ∈ On → (A +o (B +o ∅)) = (A +o B))
22	21	adantl 305	. . . . . 6 ⊢ ((A ∈ On ∧ B ∈ On) → (A +o (B +o ∅)) = (A +o B))
23	19, 22	eqtr4d 1131	. . . . 5 ⊢ ((A ∈ On ∧ B ∈ On) → ((A +o B) +o ∅) = (A +o (B +o ∅)))
24		oasuc 3131	. . . . . . . . . 10 ⊢ (((A +o B) ∈ On ∧ y ∈ On) → ((A +o B) +o suc y) = suc ((A +o B) +o y))
25	24, 17	sylan 343	. . . . . . . . 9 ⊢ (((A ∈ On ∧ B ∈ On) ∧ y ∈ On) → ((A +o B) +o suc y) = suc ((A +o B) +o y))
26		oasuc 3131	. . . . . . . . . . . . 13 ⊢ ((B ∈ On ∧ y ∈ On) → (B +o suc y) = suc (B +o y))
27	26	opreq2d 3013	. . . . . . . . . . . 12 ⊢ ((B ∈ On ∧ y ∈ On) → (A +o (B +o suc y)) = (A +o suc (B +o y)))
28	27	adantl 305	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ (B ∈ On ∧ y ∈ On)) → (A +o (B +o suc y)) = (A +o suc (B +o y)))
29		oasuc 3131	. . . . . . . . . . . 12 ⊢ ((A ∈ On ∧ (B +o y) ∈ On) → (A +o suc (B +o y)) = suc (A +o (B +o y)))
30		oacl 3138	. . . . . . . . . . . 12 ⊢ ((B ∈ On ∧ y ∈ On) → (B +o y) ∈ On)
31	29, 30	sylan2 346	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ (B ∈ On ∧ y ∈ On)) → (A +o suc (B +o y)) = suc (A +o (B +o y)))
32	28, 31	eqtrd 1128	. . . . . . . . . 10 ⊢ ((A ∈ On ∧ (B ∈ On ∧ y ∈ On)) → (A +o (B +o suc y)) = suc (A +o (B +o y)))
33	32	anassrs 338	. . . . . . . . 9 ⊢ (((A ∈ On ∧ B ∈ On) ∧ y ∈ On) → (A +o (B +o suc y)) = suc (A +o (B +o y)))
34	25, 33	cleq12d 1115	. . . . . . . 8 ⊢ (((A ∈ On ∧ B ∈ On) ∧ y ∈ 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))))
35		suceq 2288	. . . . . . . 8 ⊢ (((A +o B) +o y) = (A +o (B +o y)) → suc ((A +o B) +o y) = suc (A +o (B +o y)))
36	34, 35	syl5bir 184	. . . . . . 7 ⊢ (((A ∈ On ∧ B ∈ On) ∧ y ∈ 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	exp 291	. . . . . 6 ⊢ ((A ∈ On ∧ B ∈ On) → (y ∈ On → (((A +o B) +o y) = (A +o (B +o y)) → ((A +o B) +o suc y) = (A +o (B +o suc y)))))
38	37	com12 13	. . . . 5 ⊢ (y ∈ On → ((A ∈ On ∧ B ∈ On) → (((A +o B) +o y) = (A +o (B +o y)) → ((A +o B) +o suc y) = (A +o (B +o suc y)))))
39		iuneq2 2006	. . . . . . . 8 ⊢ (∀y ∈ x ((A +o B) +o y) = (A +o (B +o y)) → ∪y ∈ x ((A +o B) +o y) = ∪y ∈ x (A +o (B +o y)))
40	39	adantl 305	. . . . . . 7 ⊢ (((Lim x ∧ (A ∈ On ∧ B ∈ On)) ∧ ∀y ∈ x ((A +o B) +o y) = (A +o (B +o y))) → ∪y ∈ x ((A +o B) +o y) = ∪y ∈ x (A +o (B +o y)))
41		visset 1350	. . . . . . . . . . 11 ⊢ x ∈ V
42		oalim 3135	. . . . . . . . . . 11 ⊢ (((A +o B) ∈ On ∧ (x ∈ V ∧ Lim x)) → ((A +o B) +o x) = ∪y ∈ x ((A +o B) +o y))
43	41, 42	mpan21 531	. . . . . . . . . 10 ⊢ (((A +o B) ∈ On ∧ Lim x) → ((A +o B) +o x) = ∪y ∈ x ((A +o B) +o y))
44	43, 17	sylan 343	. . . . . . . . 9 ⊢ (((A ∈ On ∧ B ∈ On) ∧ Lim x) → ((A +o B) +o x) = ∪y ∈ x ((A +o B) +o y))
45	44	ancoms 334	. . . . . . . 8 ⊢ ((Lim x ∧ (A ∈ On ∧ B ∈ On)) → ((A +o B) +o x) = ∪y ∈ x ((A +o B) +o y))
46	45	adantr 306	. . . . . . 7 ⊢ (((Lim x ∧ (A ∈ On ∧ B ∈ On)) ∧ ∀y ∈ x ((A +o B) +o y) = (A +o (B +o y))) → ((A +o B) +o x) = ∪y ∈ x ((A +o B) +o y))
47		oprex 3018	. . . . . . . . . . . 12 ⊢ (B +o x) ∈ V
48		oalim 3135	. . . . . . . . . . . 12 ⊢ ((A ∈ On ∧ ((B +o x) ∈ V ∧ Lim (B +o x))) → (A +o (B +o x)) = ∪z ∈ (B +o x)(A +o z))
49	47, 48	mpan21 531	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ Lim (B +o x)) → (A +o (B +o x)) = ∪z ∈ (B +o x)(A +o z))
50		oalimcl 3162	. . . . . . . . . . . . 13 ⊢ ((B ∈ On ∧ (x ∈ V ∧ Lim x)) → Lim (B +o x))
51	41, 50	mpan21 531	. . . . . . . . . . . 12 ⊢ ((B ∈ On ∧ Lim x) → Lim (B +o x))
52	51	ancoms 334	. . . . . . . . . . 11 ⊢ ((Lim x ∧ B ∈ On) → Lim (B +o x))
53	49, 52	sylan2 346	. . . . . . . . . 10 ⊢ ((A ∈ On ∧ (Lim x ∧ B ∈ On)) → (A +o (B +o x)) = ∪z ∈ (B +o x)(A +o z))
54		limelon 2286	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ V ∧ Lim x) → x ∈ On)
55	41, 54	mpan 518	. . . . . . . . . . . . . . . . 17 ⊢ (Lim x → x ∈ On)
56		oacl 3138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((B ∈ On ∧ x ∈ On) → (B +o x) ∈ On)
57	56	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((x ∈ On ∧ B ∈ On) → (B +o x) ∈ On)
58		onelon 2223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((B +o x) ∈ On ∧ z ∈ (B +o x)) → z ∈ On)
59	58	exp 291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((B +o x) ∈ On → (z ∈ (B +o x) → z ∈ On))
60	57, 59	syl 12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((x ∈ On ∧ B ∈ On) → (z ∈ (B +o x) → z ∈ On))
61	60	adantld 307	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x ∈ On ∧ B ∈ On) → ((A ∈ On ∧ z ∈ (B +o x)) → z ∈ On))
62	61	adantl 305	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Lim x ∧ (x ∈ On ∧ B ∈ On)) → ((A ∈ On ∧ z ∈ (B +o x)) → z ∈ On))
63		ordtri2or 2328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Ord z ∧ Ord B) → (z ∈ B ∨ B ⊆ z))
64	63	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Ord B ∧ Ord z) → (z ∈ B ∨ B ⊆ z))
65		eloni 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (B ∈ On → Ord B)
66		eloni 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (z ∈ On → Ord z)
67	64, 65, 66	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((B ∈ On ∧ z ∈ On) → (z ∈ B ∨ B ⊆ z))
68	67	adantrl 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((B ∈ On ∧ (z ∈ (B +o x) ∧ z ∈ On)) → (z ∈ B ∨ B ⊆ z))
69	68	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On)) → (z ∈ B ∨ B ⊆ z))
70	69	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Lim x ∧ ((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On))) → (z ∈ B ∨ B ⊆ z))
71		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (y = ∅ → (B +o y) = (B +o ∅))
72	71	sseq2d 1528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (y = ∅ → (z ⊆ (B +o y) ↔ z ⊆ (B +o ∅)))
73	72	rcla4ev 1403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∅ ∈ x ∧ z ⊆ (B +o ∅)) → ∃y ∈ x z ⊆ (B +o y))
74		0ellim 2285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Lim x → ∅ ∈ x)
75		onelsst 2255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (B ∈ On → (z ∈ B → z ⊆ B))
76	20	sseq2d 1528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (B ∈ On → (z ⊆ (B +o ∅) ↔ z ⊆ B))
77	75, 76	sylibrd 179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (B ∈ On → (z ∈ B → z ⊆ (B +o ∅)))
78	77	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((B ∈ On ∧ z ∈ B) → z ⊆ (B +o ∅))
79	73, 74, 78	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Lim x ∧ (B ∈ On ∧ z ∈ B)) → ∃y ∈ x z ⊆ (B +o y))
80	79	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim x → (B ∈ On → (z ∈ B → ∃y ∈ x z ⊆ (B +o y))))
81	80	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Lim x ∧ B ∈ On) → (z ∈ B → ∃y ∈ x z ⊆ (B +o y)))
82	81	adantrl 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Lim x ∧ (x ∈ On ∧ B ∈ On)) → (z ∈ B → ∃y ∈ x z ⊆ (B +o y)))
83	82	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Lim x ∧ ((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On))) → (z ∈ B → ∃y ∈ x z ⊆ (B +o y)))
84		oawordex 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((B ∈ On ∧ z ∈ On) → (B ⊆ z ↔ ∃y ∈ On (B +o y) = z))
85	84	adantrl 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((B ∈ On ∧ (z ∈ (B +o x) ∧ z ∈ On)) → (B ⊆ z ↔ ∃y ∈ On (B +o y) = z))
86	85	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On)) → (B ⊆ z ↔ ∃y ∈ On (B +o y) = z))
87		oaord 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((y ∈ On ∧ x ∈ On ∧ B ∈ On) → (y ∈ x ↔ (B +o y) ∈ (B +o x)))
88	87	3expb 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((y ∈ On ∧ (x ∈ On ∧ B ∈ On)) → (y ∈ x ↔ (B +o y) ∈ (B +o x)))
89		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((B +o y) = z → ((B +o y) ∈ (B +o x) ↔ z ∈ (B +o x)))
90	88, 89	sylan9bb 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((y ∈ On ∧ (x ∈ On ∧ B ∈ On)) ∧ (B +o y) = z) → (y ∈ x ↔ z ∈ (B +o x)))
91	90	an1rs 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((y ∈ On ∧ (B +o y) = z) ∧ (x ∈ On ∧ B ∈ On)) → (y ∈ x ↔ z ∈ (B +o x)))
92	91	biimpar 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((y ∈ On ∧ (B +o y) = z) ∧ (x ∈ On ∧ B ∈ On)) ∧ z ∈ (B +o x)) → y ∈ x)
93		eqimss2 1549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((B +o y) = z → z ⊆ (B +o y))
94	93	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((y ∈ On ∧ (B +o y) = z) → z ⊆ (B +o y))
95	94	ad2antll 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((y ∈ On ∧ (B +o y) = z) ∧ (x ∈ On ∧ B ∈ On)) ∧ z ∈ (B +o x)) → z ⊆ (B +o y))
96	92, 95	jca 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((y ∈ On ∧ (B +o y) = z) ∧ (x ∈ On ∧ B ∈ On)) ∧ z ∈ (B +o x)) → (y ∈ x ∧ z ⊆ (B +o y)))
97	96	anasss 337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((y ∈ On ∧ (B +o y) = z) ∧ ((x ∈ On ∧ B ∈ On) ∧ z ∈ (B +o x))) → (y ∈ x ∧ z ⊆ (B +o y)))
98	97	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((x ∈ On ∧ B ∈ On) ∧ z ∈ (B +o x)) ∧ (y ∈ On ∧ (B +o y) = z)) → (y ∈ x ∧ z ⊆ (B +o y)))
99	98	exp 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((x ∈ On ∧ B ∈ On) ∧ z ∈ (B +o x)) → ((y ∈ On ∧ (B +o y) = z) → (y ∈ x ∧ z ⊆ (B +o y))))
100	99	r19.22dv2 1277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((x ∈ On ∧ B ∈ On) ∧ z ∈ (B +o x)) → (∃y ∈ On (B +o y) = z → ∃y ∈ x z ⊆ (B +o y)))
101	100	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On)) → (∃y ∈ On (B +o y) = z → ∃y ∈ x z ⊆ (B +o y)))
102	86, 101	sylbid 178	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On)) → (B ⊆ z → ∃y ∈ x z ⊆ (B +o y)))
103	102	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Lim x ∧ ((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On))) → (B ⊆ z → ∃y ∈ x z ⊆ (B +o y)))
104	83, 103	jaod 329	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Lim x ∧ ((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On))) → ((z ∈ B ∨ B ⊆ z) → ∃y ∈ x z ⊆ (B +o y)))
105	70, 104	mpd 46	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Lim x ∧ ((x ∈ On ∧ B ∈ On) ∧ (z ∈ (B +o x) ∧ z ∈ On))) → ∃y ∈ x z ⊆ (B +o y))
106	105	exp45 303	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Lim x → ((x ∈ On ∧ B ∈ On) → (z ∈ (B +o x) → (z ∈ On → ∃y ∈ x z ⊆ (B +o y)))))
107	106	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Lim x ∧ (x ∈ On ∧ B ∈ On)) → (z ∈ (B +o x) → (z ∈ On → ∃y ∈ x z ⊆ (B +o y))))
108	107	adantld 307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Lim x ∧ (x ∈ On ∧ B ∈ On)) → ((A ∈ On ∧ z ∈ (B +o x)) → (z ∈ On → ∃y ∈ x z ⊆ (B +o y))))
109	108	imp32 281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) → ∃y ∈ x z ⊆ (B +o y))
110		oaword 3151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((z ∈ On ∧ (B +o y) ∈ On ∧ A ∈ On) → (z ⊆ (B +o y) ↔ (A +o z) ⊆ (A +o (B +o y))))
111		pm3.27 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On) → z ∈ On)
112	111	ad2antlr 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) ∧ y ∈ x) → z ∈ On)
113		onelon 2223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((x ∈ On ∧ y ∈ x) → y ∈ On)
114	30, 113	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((B ∈ On ∧ (x ∈ On ∧ y ∈ x)) → (B +o y) ∈ On)
115	114	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (B ∈ On → (x ∈ On → (y ∈ x → (B +o y) ∈ On)))
116	115	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (x ∈ On → (B ∈ On → (y ∈ x → (B +o y) ∈ On)))
117	116	imp31 280	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((x ∈ On ∧ B ∈ On) ∧ y ∈ x) → (B +o y) ∈ On)
118	117	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ y ∈ x) → (B +o y) ∈ On)
119	118	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) ∧ y ∈ x) → (B +o y) ∈ On)
120		pm3.26 256	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((A ∈ On ∧ z ∈ (B +o x)) → A ∈ On)
121	120	adantr 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On) → A ∈ On)
122	121	ad2antlr 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) ∧ y ∈ x) → A ∈ On)
123	110, 112, 119, 122	syl3anc 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) ∧ y ∈ x) → (z ⊆ (B +o y) ↔ (A +o z) ⊆ (A +o (B +o y))))
124	123	birexdva 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) → (∃y ∈ x z ⊆ (B +o y) ↔ ∃y ∈ x (A +o z) ⊆ (A +o (B +o y))))
125	109, 124	mpbid 170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((Lim x ∧ (x ∈ On ∧ B ∈ On)) ∧ ((A ∈ On ∧ z ∈ (B +o x)) ∧ z ∈ On)) → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y)))
126	125	exp32 294	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Lim x ∧ (x ∈ On ∧ B ∈ On)) → ((A ∈ On ∧ z ∈ (B +o x)) → (z ∈ On → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y)))))
127	62, 126	mpdd 47	. . . . . . . . . . . . . . . . . 18 ⊢ ((Lim x ∧ (x ∈ On ∧ B ∈ On)) → ((A ∈ On ∧ z ∈ (B +o x)) → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y))))
128	127	exp32 294	. . . . . . . . . . . . . . . . 17 ⊢ (Lim x → (x ∈ On → (B ∈ On → ((A ∈ On ∧ z ∈ (B +o x)) → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y))))))
129	55, 128	mpd 46	. . . . . . . . . . . . . . . 16 ⊢ (Lim x → (B ∈ On → ((A ∈ On ∧ z ∈ (B +o x)) → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y)))))
130	129	exp4a 295	. . . . . . . . . . . . . . 15 ⊢ (Lim x → (B ∈ On → (A ∈ On → (z ∈ (B +o x) → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y))))))
131	130	imp31 280	. . . . . . . . . . . . . 14 ⊢ (((Lim x ∧ B ∈ On) ∧ A ∈ On) → (z ∈ (B +o x) → ∃y ∈ x (A +o z) ⊆ (A +o (B +o y))))
132	131	r19.21aiv 1259	. . . . . . . . . . . . 13 ⊢ (((Lim x ∧ B ∈ On) ∧ A ∈ On) → ∀z ∈ (B +o x)∃y ∈ x (A +o z) ⊆ (A +o (B +o y)))
133		iunss2 2021	. . . . . . . . . . . . 13 ⊢ (∀z ∈ (B +o x)∃y ∈ x (A +o z) ⊆ (A +o (B +o y)) → ∪z ∈ (B +o x)(A +o z) ⊆ ∪y ∈ x (A +o (B +o y)))
134	132, 133	syl 12	. . . . . . . . . . . 12 ⊢ (((Lim x ∧ B ∈ On) ∧ A ∈ On) → ∪z ∈ (B +o x)(A +o z) ⊆ ∪y ∈ x (A +o (B +o y)))
135	134	ancoms 334	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ (Lim x ∧ B ∈ On)) → ∪z ∈ (B +o x)(A +o z) ⊆ ∪y ∈ x (A +o (B +o y)))
136		oaordi 3148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∈ On ∧ B ∈ On) → (y ∈ x → (B +o y) ∈ (B +o x)))
137	136	anim1d 432	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ On ∧ B ∈ On) → ((y ∈ x ∧ w ∈ (A +o (B +o y))) → ((B +o y) ∈ (B +o x) ∧ w ∈ (A +o (B +o y)))))
138		opreq2 3007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z = (B +o y) → (A +o z) = (A +o (B +o y)))
139	138	eleq2d 1156	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = (B +o y) → (w ∈ (A +o z) ↔ w ∈ (A +o (B +o y))))
140	139	rcla4ev 1403	. . . . . . . . . . . . . . . . . 18 ⊢ (((B +o y) ∈ (B +o x) ∧ w ∈ (A +o (B +o y))) → ∃z ∈ (B +o x)w ∈ (A +o z))
141	137, 140	syl6 23	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ On ∧ B ∈ On) → ((y ∈ x ∧ w ∈ (A +o (B +o y))) → ∃z ∈ (B +o x)w ∈ (A +o z)))
142	141	exp3a 292	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ∧ B ∈ On) → (y ∈ x → (w ∈ (A +o (B +o y)) → ∃z ∈ (B +o x)w ∈ (A +o z))))
143	142	r19.23adv 1286	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On ∧ B ∈ On) → (∃y ∈ x w ∈ (A +o (B +o y)) → ∃z ∈ (B +o x)w ∈ (A +o z)))
144		eliun 1998	. . . . . . . . . . . . . . 15 ⊢ (w ∈ ∪y ∈ x (A +o (B +o y)) ↔ ∃y ∈ x w ∈ (A +o (B +o y)))
145		eliun 1998	. . . . . . . . . . . . . . 15 ⊢ (w ∈ ∪z ∈ (B +o x)(A +o z) ↔ ∃z ∈ (B +o x)w ∈ (A +o z))
146	143, 144, 145	3imtr4g 426	. . . . . . . . . . . . . 14 ⊢ ((x ∈ On ∧ B ∈ On) → (w ∈ ∪y ∈ x (A +o (B +o y)) → w ∈ ∪z ∈ (B +o x)(A +o z)))
147	146	ssrdv 1509	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ∧ B ∈ On) → ∪y ∈ x (A +o (B +o y)) ⊆ ∪z ∈ (B +o x)(A +o z))
148	147, 55	sylan 343	. . . . . . . . . . . 12 ⊢ ((Lim x ∧ B ∈ On) → ∪y ∈ x (A +o (B +o y)) ⊆ ∪z ∈ (B +o x)(A +o z))
149	148	adantl 305	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ (Lim x ∧ B ∈ On)) → ∪y ∈ x (A +o (B +o y)) ⊆ ∪z ∈ (B +o x)(A +o z))
150	135, 149	eqssd 1518	. . . . . . . . . 10 ⊢ ((A ∈ On ∧ (Lim x ∧ B ∈ On)) → ∪z ∈ (B +o x)(A +o z) = ∪y ∈ x (A +o (B +o y)))
151	53, 150	eqtrd 1128	. . . . . . . . 9 ⊢ ((A ∈ On ∧ (Lim x ∧ B ∈ On)) → (A +o (B +o x)) = ∪y ∈ x (A +o (B +o y)))
152	151	an1s 372	. . . . . . . 8 ⊢ ((Lim x ∧ (A ∈ On ∧ B ∈ On)) → (A +o (B +o x)) = ∪y ∈ x (A +o (B +o y)))
153	152	adantr 306	. . . . . . 7 ⊢ (((Lim x ∧ (A ∈ On ∧ B ∈ On)) ∧ ∀y ∈ x ((A +o B) +o y) = (A +o (B +o y))) → (A +o (B +o x)) = ∪y ∈ x (A +o (B +o y)))
154	40, 46, 153	3eqtr4d 1134	. . . . . 6 ⊢ (((Lim x ∧ (A ∈ On ∧ B ∈ On)) ∧ ∀y ∈ x ((A +o B) +o y) = (A +o (B +o y))) → ((A +o B) +o x) = (A +o (B +o x)))
155	154	exp31 293	. . . . 5 ⊢ (Lim x → ((A ∈ On ∧ B ∈ On) → (∀y ∈ x ((A +o B) +o y) = (A +o (B +o y)) → ((A +o B) +o x) = (A +o (B +o x)))))
156	4, 8, 12, 16, 23, 38, 155	tfinds3 2406	. . . 4 ⊢ (C ∈ On → ((A ∈ On ∧ B ∈ On) → ((A +o B) +o C) = (A +o (B +o C))))
157	156	com12 13	. . 3 ⊢ ((A ∈ On ∧ B ∈ On) → (C ∈ On → ((A +o B) +o C) = (A +o (B +o C))))
158	157	exp 291	. 2 ⊢ (A ∈ On → (B ∈ On → (C ∈ On → ((A +o B) +o C) = (A +o (B +o C)))))
159	158	3imp 608	1 ⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → ((A +o B) +o C) = (A +o (B +o C)))

Syntax hints:   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196   ∧ w3a 581   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ∪ciun 1994  Ord word 2198  Oncon0 2199  Lim wlim 2200  suc csuc 2201  (class class class)co 3001   +_o coa 3101

This theorem is referenced by:  nnaass 3179

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 199