oaass

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

		Ref	Expression
	Assertion	oaass	$⊢ (A \in On \land B \in On \land C \in On) \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} \emptyset$
2		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
3	2	oveq2d	$⊢ x = \emptyset \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} \emptyset)$
4	1 3	eqeq12d	$⊢ x = \emptyset \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} (B +_{𝑜} \emptyset))$
5		oveq2	$⊢ x = y \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} y$
6		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
7	6	oveq2d	$⊢ x = y \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} y)$
8	5 7	eqeq12d	$⊢ x = y \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y))$
9		oveq2	$⊢ x = suc y \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} suc y$
10		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
11	10	oveq2d	$⊢ x = suc y \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} suc y)$
12	9 11	eqeq12d	$⊢ x = suc y \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y))$
13		oveq2	$⊢ x = C \to (A +_{𝑜} B) +_{𝑜} x = (A +_{𝑜} B) +_{𝑜} C$
14		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
15	14	oveq2d	$⊢ x = C \to A +_{𝑜} (B +_{𝑜} x) = A +_{𝑜} (B +_{𝑜} C)$
16	13 15	eqeq12d	$⊢ x = C \to ((A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x) \leftrightarrow (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C))$
17		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
18		oa0	$⊢ A +_{𝑜} B \in On \to (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} B$
19	17 18	syl	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} B$
20		oa0	$⊢ B \in On \to B +_{𝑜} \emptyset = B$
21	20	oveq2d	$⊢ B \in On \to A +_{𝑜} (B +_{𝑜} \emptyset) = A +_{𝑜} B$
22	21	adantl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} (B +_{𝑜} \emptyset) = A +_{𝑜} B$
23	19 22	eqtr4d	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B) +_{𝑜} \emptyset = A +_{𝑜} (B +_{𝑜} \emptyset)$
24		suceq	$⊢ (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to suc ((A +_{𝑜} B) +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y))$
25		oasuc	$⊢ (A +_{𝑜} B \in On \land y \in On) \to (A +_{𝑜} B) +_{𝑜} suc y = suc ((A +_{𝑜} B) +_{𝑜} y)$
26	17 25	sylan	$⊢ ((A \in On \land B \in On) \land y \in On) \to (A +_{𝑜} B) +_{𝑜} suc y = suc ((A +_{𝑜} B) +_{𝑜} y)$
27		oasuc	$⊢ (B \in On \land y \in On) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
28	27	oveq2d	$⊢ (B \in On \land y \in On) \to A +_{𝑜} (B +_{𝑜} suc y) = A +_{𝑜} suc (B +_{𝑜} y)$
29	28	adantl	$⊢ (A \in On \land (B \in On \land y \in On)) \to A +_{𝑜} (B +_{𝑜} suc y) = A +_{𝑜} suc (B +_{𝑜} y)$
30		oacl	$⊢ (B \in On \land y \in On) \to B +_{𝑜} y \in On$
31		oasuc	$⊢ (A \in On \land B +_{𝑜} y \in On) \to A +_{𝑜} suc (B +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y))$
32	30 31	sylan2	$⊢ (A \in On \land (B \in On \land y \in On)) \to A +_{𝑜} suc (B +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y))$
33	29 32	eqtrd	$⊢ (A \in On \land (B \in On \land y \in On)) \to A +_{𝑜} (B +_{𝑜} suc y) = suc (A +_{𝑜} (B +_{𝑜} y))$
34	33	anassrs	$⊢ ((A \in On \land B \in On) \land y \in On) \to A +_{𝑜} (B +_{𝑜} suc y) = suc (A +_{𝑜} (B +_{𝑜} y))$
35	26 34	eqeq12d	$⊢ ((A \in On \land B \in On) \land y \in On) \to ((A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y) \leftrightarrow suc ((A +_{𝑜} B) +_{𝑜} y) = suc (A +_{𝑜} (B +_{𝑜} y)))$
36	24 35	imbitrrid	$⊢ ((A \in On \land B \in On) \land y \in On) \to ((A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to (A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y))$
37	36	expcom	$⊢ y \in On \to ((A \in On \land B \in On) \to ((A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to (A +_{𝑜} B) +_{𝑜} suc y = A +_{𝑜} (B +_{𝑜} suc y)))$
38		iuneq2	$⊢ \forall y \in x (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y) = ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
39	38	adantl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y)) \to ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y) = ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
40		vex	$⊢ x \in V$
41		oalim	$⊢ (A +_{𝑜} B \in On \land (x \in V \land Lim x)) \to (A +_{𝑜} B) +_{𝑜} x = ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y)$
42	40 41	mpanr1	$⊢ (A +_{𝑜} B \in On \land Lim x) \to (A +_{𝑜} B) +_{𝑜} x = ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y)$
43	17 42	sylan	$⊢ ((A \in On \land B \in On) \land Lim x) \to (A +_{𝑜} B) +_{𝑜} x = ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y)$
44	43	ancoms	$⊢ (Lim x \land (A \in On \land B \in On)) \to (A +_{𝑜} B) +_{𝑜} x = ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y)$
45	44	adantr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y)) \to (A +_{𝑜} B) +_{𝑜} x = ⋃_{y \in x} ((A +_{𝑜} B) +_{𝑜} y)$
46		oalimcl	$⊢ (B \in On \land (x \in V \land Lim x)) \to Lim (B +_{𝑜} x)$
47	40 46	mpanr1	$⊢ (B \in On \land Lim x) \to Lim (B +_{𝑜} x)$
48	47	ancoms	$⊢ (Lim x \land B \in On) \to Lim (B +_{𝑜} x)$
49		ovex	$⊢ B +_{𝑜} x \in V$
50		oalim	$⊢ (A \in On \land (B +_{𝑜} x \in V \land Lim (B +_{𝑜} x))) \to A +_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z)$
51	49 50	mpanr1	$⊢ (A \in On \land Lim (B +_{𝑜} x)) \to A +_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z)$
52	48 51	sylan2	$⊢ (A \in On \land (Lim x \land B \in On)) \to A +_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z)$
53		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
54	40 53	mpan	$⊢ Lim x \to x \in On$
55		oacl	$⊢ (B \in On \land x \in On) \to B +_{𝑜} x \in On$
56	55	ancoms	$⊢ (x \in On \land B \in On) \to B +_{𝑜} x \in On$
57		onelon	$⊢ (B +_{𝑜} x \in On \land z \in (B +_{𝑜} x)) \to z \in On$
58	57	ex	$⊢ B +_{𝑜} x \in On \to (z \in (B +_{𝑜} x) \to z \in On)$
59	56 58	syl	$⊢ (x \in On \land B \in On) \to (z \in (B +_{𝑜} x) \to z \in On)$
60	59	adantld	$⊢ (x \in On \land B \in On) \to ((A \in On \land z \in (B +_{𝑜} x)) \to z \in On)$
61	60	adantl	$⊢ (Lim x \land (x \in On \land B \in On)) \to ((A \in On \land z \in (B +_{𝑜} x)) \to z \in On)$
62		0ellim	$⊢ Lim x \to \emptyset \in x$
63		onelss	$⊢ B \in On \to (z \in B \to z \subseteq B)$
64	20	sseq2d	$⊢ B \in On \to (z \subseteq B +_{𝑜} \emptyset \leftrightarrow z \subseteq B)$
65	63 64	sylibrd	$⊢ B \in On \to (z \in B \to z \subseteq B +_{𝑜} \emptyset)$
66	65	imp	$⊢ (B \in On \land z \in B) \to z \subseteq B +_{𝑜} \emptyset$
67		oveq2	$⊢ y = \emptyset \to B +_{𝑜} y = B +_{𝑜} \emptyset$
68	67	sseq2d	$⊢ y = \emptyset \to (z \subseteq B +_{𝑜} y \leftrightarrow z \subseteq B +_{𝑜} \emptyset)$
69	68	rspcev	$⊢ (\emptyset \in x \land z \subseteq B +_{𝑜} \emptyset) \to \exists y \in x z \subseteq B +_{𝑜} y$
70	62 66 69	syl2an	$⊢ (Lim x \land (B \in On \land z \in B)) \to \exists y \in x z \subseteq B +_{𝑜} y$
71	70	expr	$⊢ (Lim x \land B \in On) \to (z \in B \to \exists y \in x z \subseteq B +_{𝑜} y)$
72	71	adantrl	$⊢ (Lim x \land (x \in On \land B \in On)) \to (z \in B \to \exists y \in x z \subseteq B +_{𝑜} y)$
73	72	adantrr	$⊢ (Lim x \land ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On))) \to (z \in B \to \exists y \in x z \subseteq B +_{𝑜} y)$
74		oawordex	$⊢ (B \in On \land z \in On) \to (B \subseteq z \leftrightarrow \exists y \in On B +_{𝑜} y = z)$
75	74	ad2ant2l	$⊢ ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On)) \to (B \subseteq z \leftrightarrow \exists y \in On B +_{𝑜} y = z)$
76		oaord	$⊢ (y \in On \land x \in On \land B \in On) \to (y \in x \leftrightarrow B +_{𝑜} y \in (B +_{𝑜} x))$
77	76	3expb	$⊢ (y \in On \land (x \in On \land B \in On)) \to (y \in x \leftrightarrow B +_{𝑜} y \in (B +_{𝑜} x))$
78		eleq1	$⊢ B +_{𝑜} y = z \to (B +_{𝑜} y \in (B +_{𝑜} x) \leftrightarrow z \in (B +_{𝑜} x))$
79	77 78	sylan9bb	$⊢ ((y \in On \land (x \in On \land B \in On)) \land B +_{𝑜} y = z) \to (y \in x \leftrightarrow z \in (B +_{𝑜} x))$
80	79	an32s	$⊢ ((y \in On \land B +_{𝑜} y = z) \land (x \in On \land B \in On)) \to (y \in x \leftrightarrow z \in (B +_{𝑜} x))$
81	80	biimpar	$⊢ (((y \in On \land B +_{𝑜} y = z) \land (x \in On \land B \in On)) \land z \in (B +_{𝑜} x)) \to y \in x$
82		eqimss2	$⊢ B +_{𝑜} y = z \to z \subseteq B +_{𝑜} y$
83	82	ad3antlr	$⊢ (((y \in On \land B +_{𝑜} y = z) \land (x \in On \land B \in On)) \land z \in (B +_{𝑜} x)) \to z \subseteq B +_{𝑜} y$
84	81 83	jca	$⊢ (((y \in On \land B +_{𝑜} y = z) \land (x \in On \land B \in On)) \land z \in (B +_{𝑜} x)) \to (y \in x \land z \subseteq B +_{𝑜} y)$
85	84	anasss	$⊢ ((y \in On \land B +_{𝑜} y = z) \land ((x \in On \land B \in On) \land z \in (B +_{𝑜} x))) \to (y \in x \land z \subseteq B +_{𝑜} y)$
86	85	expcom	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to ((y \in On \land B +_{𝑜} y = z) \to (y \in x \land z \subseteq B +_{𝑜} y))$
87	86	reximdv2	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to (\exists y \in On B +_{𝑜} y = z \to \exists y \in x z \subseteq B +_{𝑜} y)$
88	87	adantrr	$⊢ ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On)) \to (\exists y \in On B +_{𝑜} y = z \to \exists y \in x z \subseteq B +_{𝑜} y)$
89	75 88	sylbid	$⊢ ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On)) \to (B \subseteq z \to \exists y \in x z \subseteq B +_{𝑜} y)$
90	89	adantl	$⊢ (Lim x \land ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On))) \to (B \subseteq z \to \exists y \in x z \subseteq B +_{𝑜} y)$
91		eloni	$⊢ z \in On \to Ord z$
92		eloni	$⊢ B \in On \to Ord B$
93		ordtri2or	$⊢ (Ord z \land Ord B) \to (z \in B \lor B \subseteq z)$
94	91 92 93	syl2anr	$⊢ (B \in On \land z \in On) \to (z \in B \lor B \subseteq z)$
95	94	ad2ant2l	$⊢ ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On)) \to (z \in B \lor B \subseteq z)$
96	95	adantl	$⊢ (Lim x \land ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On))) \to (z \in B \lor B \subseteq z)$
97	73 90 96	mpjaod	$⊢ (Lim x \land ((x \in On \land B \in On) \land (z \in (B +_{𝑜} x) \land z \in On))) \to \exists y \in x z \subseteq B +_{𝑜} y$
98	97	exp45	$⊢ Lim x \to ((x \in On \land B \in On) \to (z \in (B +_{𝑜} x) \to (z \in On \to \exists y \in x z \subseteq B +_{𝑜} y)))$
99	98	imp	$⊢ (Lim x \land (x \in On \land B \in On)) \to (z \in (B +_{𝑜} x) \to (z \in On \to \exists y \in x z \subseteq B +_{𝑜} y))$
100	99	adantld	$⊢ (Lim x \land (x \in On \land B \in On)) \to ((A \in On \land z \in (B +_{𝑜} x)) \to (z \in On \to \exists y \in x z \subseteq B +_{𝑜} y))$
101	100	imp32	$⊢ ((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \to \exists y \in x z \subseteq B +_{𝑜} y$
102		simplrr	$⊢ (((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \land y \in x) \to z \in On$
103		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
104	103 30	sylan2	$⊢ (B \in On \land (x \in On \land y \in x)) \to B +_{𝑜} y \in On$
105	104	exp32	$⊢ B \in On \to (x \in On \to (y \in x \to B +_{𝑜} y \in On))$
106	105	com12	$⊢ x \in On \to (B \in On \to (y \in x \to B +_{𝑜} y \in On))$
107	106	imp31	$⊢ ((x \in On \land B \in On) \land y \in x) \to B +_{𝑜} y \in On$
108	107	ad4ant24	$⊢ (((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \land y \in x) \to B +_{𝑜} y \in On$
109		simpll	$⊢ ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On) \to A \in On$
110	109	ad2antlr	$⊢ (((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \land y \in x) \to A \in On$
111		oaword	$⊢ (z \in On \land B +_{𝑜} y \in On \land A \in On) \to (z \subseteq B +_{𝑜} y \leftrightarrow A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))$
112	102 108 110 111	syl3anc	$⊢ (((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \land y \in x) \to (z \subseteq B +_{𝑜} y \leftrightarrow A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))$
113	112	rexbidva	$⊢ ((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \to (\exists y \in x z \subseteq B +_{𝑜} y \leftrightarrow \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))$
114	101 113	mpbid	$⊢ ((Lim x \land (x \in On \land B \in On)) \land ((A \in On \land z \in (B +_{𝑜} x)) \land z \in On)) \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y)$
115	114	exp32	$⊢ (Lim x \land (x \in On \land B \in On)) \to ((A \in On \land z \in (B +_{𝑜} x)) \to (z \in On \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y)))$
116	61 115	mpdd	$⊢ (Lim x \land (x \in On \land B \in On)) \to ((A \in On \land z \in (B +_{𝑜} x)) \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))$
117	116	exp32	$⊢ Lim x \to (x \in On \to (B \in On \to ((A \in On \land z \in (B +_{𝑜} x)) \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))))$
118	54 117	mpd	$⊢ Lim x \to (B \in On \to ((A \in On \land z \in (B +_{𝑜} x)) \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y)))$
119	118	exp4a	$⊢ Lim x \to (B \in On \to (A \in On \to (z \in (B +_{𝑜} x) \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))))$
120	119	imp31	$⊢ ((Lim x \land B \in On) \land A \in On) \to (z \in (B +_{𝑜} x) \to \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y))$
121	120	ralrimiv	$⊢ ((Lim x \land B \in On) \land A \in On) \to \forall z \in (B +_{𝑜} x) \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y)$
122		iunss2	$⊢ \forall z \in (B +_{𝑜} x) \exists y \in x A +_{𝑜} z \subseteq A +_{𝑜} (B +_{𝑜} y) \to ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z) \subseteq ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
123	121 122	syl	$⊢ ((Lim x \land B \in On) \land A \in On) \to ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z) \subseteq ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
124	123	ancoms	$⊢ (A \in On \land (Lim x \land B \in On)) \to ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z) \subseteq ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
125		oaordi	$⊢ (x \in On \land B \in On) \to (y \in x \to B +_{𝑜} y \in (B +_{𝑜} x))$
126	125	anim1d	$⊢ (x \in On \land B \in On) \to ((y \in x \land w \in (A +_{𝑜} (B +_{𝑜} y))) \to (B +_{𝑜} y \in (B +_{𝑜} x) \land w \in (A +_{𝑜} (B +_{𝑜} y))))$
127		oveq2	$⊢ z = B +_{𝑜} y \to A +_{𝑜} z = A +_{𝑜} (B +_{𝑜} y)$
128	127	eleq2d	$⊢ z = B +_{𝑜} y \to (w \in (A +_{𝑜} z) \leftrightarrow w \in (A +_{𝑜} (B +_{𝑜} y)))$
129	128	rspcev	$⊢ (B +_{𝑜} y \in (B +_{𝑜} x) \land w \in (A +_{𝑜} (B +_{𝑜} y))) \to \exists z \in (B +_{𝑜} x) w \in (A +_{𝑜} z)$
130	126 129	syl6	$⊢ (x \in On \land B \in On) \to ((y \in x \land w \in (A +_{𝑜} (B +_{𝑜} y))) \to \exists z \in (B +_{𝑜} x) w \in (A +_{𝑜} z))$
131	130	expd	$⊢ (x \in On \land B \in On) \to (y \in x \to (w \in (A +_{𝑜} (B +_{𝑜} y)) \to \exists z \in (B +_{𝑜} x) w \in (A +_{𝑜} z)))$
132	131	rexlimdv	$⊢ (x \in On \land B \in On) \to (\exists y \in x w \in (A +_{𝑜} (B +_{𝑜} y)) \to \exists z \in (B +_{𝑜} x) w \in (A +_{𝑜} z))$
133		eliun	$⊢ w \in ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y)) \leftrightarrow \exists y \in x w \in (A +_{𝑜} (B +_{𝑜} y))$
134		eliun	$⊢ w \in ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z) \leftrightarrow \exists z \in (B +_{𝑜} x) w \in (A +_{𝑜} z)$
135	132 133 134	3imtr4g	$⊢ (x \in On \land B \in On) \to (w \in ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y)) \to w \in ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z))$
136	135	ssrdv	$⊢ (x \in On \land B \in On) \to ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y)) \subseteq ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z)$
137	54 136	sylan	$⊢ (Lim x \land B \in On) \to ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y)) \subseteq ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z)$
138	137	adantl	$⊢ (A \in On \land (Lim x \land B \in On)) \to ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y)) \subseteq ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z)$
139	124 138	eqssd	$⊢ (A \in On \land (Lim x \land B \in On)) \to ⋃_{z \in B +_{𝑜} x} (A +_{𝑜} z) = ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
140	52 139	eqtrd	$⊢ (A \in On \land (Lim x \land B \in On)) \to A +_{𝑜} (B +_{𝑜} x) = ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
141	140	an12s	$⊢ (Lim x \land (A \in On \land B \in On)) \to A +_{𝑜} (B +_{𝑜} x) = ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
142	141	adantr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y)) \to A +_{𝑜} (B +_{𝑜} x) = ⋃_{y \in x} (A +_{𝑜} (B +_{𝑜} y))$
143	39 45 142	3eqtr4d	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y)) \to (A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x)$
144	143	exp31	$⊢ Lim x \to ((A \in On \land B \in On) \to (\forall y \in x (A +_{𝑜} B) +_{𝑜} y = A +_{𝑜} (B +_{𝑜} y) \to (A +_{𝑜} B) +_{𝑜} x = A +_{𝑜} (B +_{𝑜} x)))$
145	4 8 12 16 23 37 144	tfinds3	$⊢ C \in On \to ((A \in On \land B \in On) \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C))$
146	145	com12	$⊢ (A \in On \land B \in On) \to (C \in On \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C))$
147	146	3impia	$⊢ (A \in On \land B \in On \land C \in On) \to (A +_{𝑜} B) +_{𝑜} C = A +_{𝑜} (B +_{𝑜} C)$

Metamath Proof Explorer

Theorem oaass

Proof