odi

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
2	1	oveq2d	$⊢ x = \emptyset \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} \emptyset)$
3		oveq2	$⊢ x = \emptyset \to A \cdot_{𝑜} x = A \cdot_{𝑜} \emptyset$
4	3	oveq2d	$⊢ x = \emptyset \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset)$
5	2 4	eqeq12d	$⊢ x = \emptyset \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset))$
6		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
7	6	oveq2d	$⊢ x = y \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} y)$
8		oveq2	$⊢ x = y \to A \cdot_{𝑜} x = A \cdot_{𝑜} y$
9	8	oveq2d	$⊢ x = y \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)$
10	7 9	eqeq12d	$⊢ x = y \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))$
11		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
12	11	oveq2d	$⊢ x = suc y \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} suc y)$
13		oveq2	$⊢ x = suc y \to A \cdot_{𝑜} x = A \cdot_{𝑜} suc y$
14	13	oveq2d	$⊢ x = suc y \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y)$
15	12 14	eqeq12d	$⊢ x = suc y \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))$
16		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
17	16	oveq2d	$⊢ x = C \to A \cdot_{𝑜} (B +_{𝑜} x) = A \cdot_{𝑜} (B +_{𝑜} C)$
18		oveq2	$⊢ x = C \to A \cdot_{𝑜} x = A \cdot_{𝑜} C$
19	18	oveq2d	$⊢ x = C \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)$
20	17 19	eqeq12d	$⊢ x = C \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C))$
21		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
22		oa0	$⊢ A \cdot_{𝑜} B \in On \to (A \cdot_{𝑜} B) +_{𝑜} \emptyset = A \cdot_{𝑜} B$
23	21 22	syl	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B) +_{𝑜} \emptyset = A \cdot_{𝑜} B$
24		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
25	24	adantr	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} \emptyset = \emptyset$
26	25	oveq2d	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} \emptyset$
27		oa0	$⊢ B \in On \to B +_{𝑜} \emptyset = B$
28	27	adantl	$⊢ (A \in On \land B \in On) \to B +_{𝑜} \emptyset = B$
29	28	oveq2d	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} (B +_{𝑜} \emptyset) = A \cdot_{𝑜} B$
30	23 26 29	3eqtr4rd	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} (B +_{𝑜} \emptyset) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} \emptyset)$
31		oveq1	$⊢ A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A = ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A$
32		oasuc	$⊢ (B \in On \land y \in On) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
33	32	3adant1	$⊢ (A \in On \land B \in On \land y \in On) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
34	33	oveq2d	$⊢ (A \in On \land B \in On \land y \in On) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = A \cdot_{𝑜} suc (B +_{𝑜} y)$
35		oacl	$⊢ (B \in On \land y \in On) \to B +_{𝑜} y \in On$
36		omsuc	$⊢ (A \in On \land B +_{𝑜} y \in On) \to A \cdot_{𝑜} suc (B +_{𝑜} y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
37	35 36	sylan2	$⊢ (A \in On \land (B \in On \land y \in On)) \to A \cdot_{𝑜} suc (B +_{𝑜} y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
38	37	3impb	$⊢ (A \in On \land B \in On \land y \in On) \to A \cdot_{𝑜} suc (B +_{𝑜} y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
39	34 38	eqtrd	$⊢ (A \in On \land B \in On \land y \in On) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A$
40		omsuc	$⊢ (A \in On \land y \in On) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
41	40	3adant2	$⊢ (A \in On \land B \in On \land y \in On) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
42	41	oveq2d	$⊢ (A \in On \land B \in On \land y \in On) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
43		omcl	$⊢ (A \in On \land y \in On) \to A \cdot_{𝑜} y \in On$
44		oaass	$⊢ (A \cdot_{𝑜} B \in On \land A \cdot_{𝑜} y \in On \land A \in On) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
45	21 44	syl3an1	$⊢ ((A \in On \land B \in On) \land A \cdot_{𝑜} y \in On \land A \in On) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
46	43 45	syl3an2	$⊢ ((A \in On \land B \in On) \land (A \in On \land y \in On) \land A \in On) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
47	46	3exp	$⊢ (A \in On \land B \in On) \to ((A \in On \land y \in On) \to (A \in On \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)))$
48	47	exp4b	$⊢ A \in On \to (B \in On \to (A \in On \to (y \in On \to (A \in On \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)))))$
49	48	pm2.43a	$⊢ A \in On \to (B \in On \to (y \in On \to (A \in On \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A))))$
50	49	com4r	$⊢ A \in On \to (A \in On \to (B \in On \to (y \in On \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A))))$
51	50	pm2.43i	$⊢ A \in On \to (B \in On \to (y \in On \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)))$
52	51	3imp	$⊢ (A \in On \land B \in On \land y \in On) \to ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} ((A \cdot_{𝑜} y) +_{𝑜} A)$
53	42 52	eqtr4d	$⊢ (A \in On \land B \in On \land y \in On) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y) = ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A$
54	39 53	eqeq12d	$⊢ (A \in On \land B \in On \land y \in On) \to (A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y) \leftrightarrow (A \cdot_{𝑜} (B +_{𝑜} y)) +_{𝑜} A = ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) +_{𝑜} A)$
55	31 54	syl5ibr	$⊢ (A \in On \land B \in On \land y \in On) \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))$
56	55	3exp	$⊢ A \in On \to (B \in On \to (y \in On \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))))$
57	56	com3r	$⊢ y \in On \to (A \in On \to (B \in On \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y))))$
58	57	impd	$⊢ y \in On \to ((A \in On \land B \in On) \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} suc y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} suc y)))$
59		vex	$⊢ x \in V$
60		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
61	59 60	mpan	$⊢ Lim x \to x \in On$
62		oacl	$⊢ (B \in On \land x \in On) \to B +_{𝑜} x \in On$
63		om0r	$⊢ B +_{𝑜} x \in On \to \emptyset \cdot_{𝑜} (B +_{𝑜} x) = \emptyset$
64	62 63	syl	$⊢ (B \in On \land x \in On) \to \emptyset \cdot_{𝑜} (B +_{𝑜} x) = \emptyset$
65		om0r	$⊢ B \in On \to \emptyset \cdot_{𝑜} B = \emptyset$
66		om0r	$⊢ x \in On \to \emptyset \cdot_{𝑜} x = \emptyset$
67	65 66	oveqan12d	$⊢ (B \in On \land x \in On) \to (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x) = \emptyset +_{𝑜} \emptyset$
68		0elon	$⊢ \emptyset \in On$
69		oa0	$⊢ \emptyset \in On \to \emptyset +_{𝑜} \emptyset = \emptyset$
70	68 69	ax-mp	$⊢ \emptyset +_{𝑜} \emptyset = \emptyset$
71	67 70	syl6req	$⊢ (B \in On \land x \in On) \to \emptyset = (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x)$
72	64 71	eqtrd	$⊢ (B \in On \land x \in On) \to \emptyset \cdot_{𝑜} (B +_{𝑜} x) = (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x)$
73	61 72	sylan2	$⊢ (B \in On \land Lim x) \to \emptyset \cdot_{𝑜} (B +_{𝑜} x) = (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x)$
74	73	ancoms	$⊢ (Lim x \land B \in On) \to \emptyset \cdot_{𝑜} (B +_{𝑜} x) = (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x)$
75		oveq1	$⊢ A = \emptyset \to A \cdot_{𝑜} (B +_{𝑜} x) = \emptyset \cdot_{𝑜} (B +_{𝑜} x)$
76		oveq1	$⊢ A = \emptyset \to A \cdot_{𝑜} B = \emptyset \cdot_{𝑜} B$
77		oveq1	$⊢ A = \emptyset \to A \cdot_{𝑜} x = \emptyset \cdot_{𝑜} x$
78	76 77	oveq12d	$⊢ A = \emptyset \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x)$
79	75 78	eqeq12d	$⊢ A = \emptyset \to (A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) \leftrightarrow \emptyset \cdot_{𝑜} (B +_{𝑜} x) = (\emptyset \cdot_{𝑜} B) +_{𝑜} (\emptyset \cdot_{𝑜} x))$
80	74 79	syl5ibr	$⊢ A = \emptyset \to ((Lim x \land B \in On) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x))$
81	80	expd	$⊢ A = \emptyset \to (Lim x \to (B \in On \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)))$
82	81	com3r	$⊢ B \in On \to (A = \emptyset \to (Lim x \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)))$
83	82	imp	$⊢ (B \in On \land A = \emptyset) \to (Lim x \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x))$
84	83	a1dd	$⊢ (B \in On \land A = \emptyset) \to (Lim x \to (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)))$
85		simplr	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to B \in On$
86	62	ancoms	$⊢ (x \in On \land B \in On) \to B +_{𝑜} x \in On$
87		onelon	$⊢ (B +_{𝑜} x \in On \land z \in (B +_{𝑜} x)) \to z \in On$
88	86 87	sylan	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to z \in On$
89		ontri1	$⊢ (B \in On \land z \in On) \to (B \subseteq z \leftrightarrow \neg z \in B)$
90		oawordex	$⊢ (B \in On \land z \in On) \to (B \subseteq z \leftrightarrow \exists v \in On B +_{𝑜} v = z)$
91	89 90	bitr3d	$⊢ (B \in On \land z \in On) \to (\neg z \in B \leftrightarrow \exists v \in On B +_{𝑜} v = z)$
92	85 88 91	syl2anc	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to (\neg z \in B \leftrightarrow \exists v \in On B +_{𝑜} v = z)$
93		oaord	$⊢ (v \in On \land x \in On \land B \in On) \to (v \in x \leftrightarrow B +_{𝑜} v \in (B +_{𝑜} x))$
94	93	3expb	$⊢ (v \in On \land (x \in On \land B \in On)) \to (v \in x \leftrightarrow B +_{𝑜} v \in (B +_{𝑜} x))$
95		eleq1	$⊢ B +_{𝑜} v = z \to (B +_{𝑜} v \in (B +_{𝑜} x) \leftrightarrow z \in (B +_{𝑜} x))$
96	94 95	sylan9bb	$⊢ ((v \in On \land (x \in On \land B \in On)) \land B +_{𝑜} v = z) \to (v \in x \leftrightarrow z \in (B +_{𝑜} x))$
97		iba	$⊢ B +_{𝑜} v = z \to (v \in x \leftrightarrow (v \in x \land B +_{𝑜} v = z))$
98	97	adantl	$⊢ ((v \in On \land (x \in On \land B \in On)) \land B +_{𝑜} v = z) \to (v \in x \leftrightarrow (v \in x \land B +_{𝑜} v = z))$
99	96 98	bitr3d	$⊢ ((v \in On \land (x \in On \land B \in On)) \land B +_{𝑜} v = z) \to (z \in (B +_{𝑜} x) \leftrightarrow (v \in x \land B +_{𝑜} v = z))$
100	99	an32s	$⊢ ((v \in On \land B +_{𝑜} v = z) \land (x \in On \land B \in On)) \to (z \in (B +_{𝑜} x) \leftrightarrow (v \in x \land B +_{𝑜} v = z))$
101	100	biimpcd	$⊢ z \in (B +_{𝑜} x) \to (((v \in On \land B +_{𝑜} v = z) \land (x \in On \land B \in On)) \to (v \in x \land B +_{𝑜} v = z))$
102	101	exp4c	$⊢ z \in (B +_{𝑜} x) \to (v \in On \to (B +_{𝑜} v = z \to ((x \in On \land B \in On) \to (v \in x \land B +_{𝑜} v = z))))$
103	102	com4r	$⊢ (x \in On \land B \in On) \to (z \in (B +_{𝑜} x) \to (v \in On \to (B +_{𝑜} v = z \to (v \in x \land B +_{𝑜} v = z))))$
104	103	imp	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to (v \in On \to (B +_{𝑜} v = z \to (v \in x \land B +_{𝑜} v = z)))$
105	104	reximdvai	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to (\exists v \in On B +_{𝑜} v = z \to \exists v \in On (v \in x \land B +_{𝑜} v = z))$
106	92 105	sylbid	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to (\neg z \in B \to \exists v \in On (v \in x \land B +_{𝑜} v = z))$
107	106	orrd	$⊢ ((x \in On \land B \in On) \land z \in (B +_{𝑜} x)) \to (z \in B \lor \exists v \in On (v \in x \land B +_{𝑜} v = z))$
108	61 107	sylanl1	$⊢ ((Lim x \land B \in On) \land z \in (B +_{𝑜} x)) \to (z \in B \lor \exists v \in On (v \in x \land B +_{𝑜} v = z))$
109	108	adantlrl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land z \in (B +_{𝑜} x)) \to (z \in B \lor \exists v \in On (v \in x \land B +_{𝑜} v = z))$
110	109	adantlr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \land z \in (B +_{𝑜} x)) \to (z \in B \lor \exists v \in On (v \in x \land B +_{𝑜} v = z))$
111		0ellim	$⊢ Lim x \to \emptyset \in x$
112		om00el	$⊢ (A \in On \land x \in On) \to (\emptyset \in (A \cdot_{𝑜} x) \leftrightarrow (\emptyset \in A \land \emptyset \in x))$
113	112	biimprd	$⊢ (A \in On \land x \in On) \to ((\emptyset \in A \land \emptyset \in x) \to \emptyset \in (A \cdot_{𝑜} x))$
114	111 113	sylan2i	$⊢ (A \in On \land x \in On) \to ((\emptyset \in A \land Lim x) \to \emptyset \in (A \cdot_{𝑜} x))$
115	61 114	sylan2	$⊢ (A \in On \land Lim x) \to ((\emptyset \in A \land Lim x) \to \emptyset \in (A \cdot_{𝑜} x))$
116	115	exp4b	$⊢ A \in On \to (Lim x \to (\emptyset \in A \to (Lim x \to \emptyset \in (A \cdot_{𝑜} x))))$
117	116	com4r	$⊢ Lim x \to (A \in On \to (Lim x \to (\emptyset \in A \to \emptyset \in (A \cdot_{𝑜} x))))$
118	117	pm2.43a	$⊢ Lim x \to (A \in On \to (\emptyset \in A \to \emptyset \in (A \cdot_{𝑜} x)))$
119	118	imp31	$⊢ ((Lim x \land A \in On) \land \emptyset \in A) \to \emptyset \in (A \cdot_{𝑜} x)$
120	119	a1d	$⊢ ((Lim x \land A \in On) \land \emptyset \in A) \to (z \in B \to \emptyset \in (A \cdot_{𝑜} x))$
121	120	adantlrr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to (z \in B \to \emptyset \in (A \cdot_{𝑜} x))$
122		omordi	$⊢ ((B \in On \land A \in On) \land \emptyset \in A) \to (z \in B \to A \cdot_{𝑜} z \in (A \cdot_{𝑜} B))$
123	122	ancom1s	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to (z \in B \to A \cdot_{𝑜} z \in (A \cdot_{𝑜} B))$
124		onelss	$⊢ A \cdot_{𝑜} B \in On \to (A \cdot_{𝑜} z \in (A \cdot_{𝑜} B) \to A \cdot_{𝑜} z \subseteq A \cdot_{𝑜} B)$
125	22	sseq2d	$⊢ A \cdot_{𝑜} B \in On \to (A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset \leftrightarrow A \cdot_{𝑜} z \subseteq A \cdot_{𝑜} B)$
126	124 125	sylibrd	$⊢ A \cdot_{𝑜} B \in On \to (A \cdot_{𝑜} z \in (A \cdot_{𝑜} B) \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset)$
127	21 126	syl	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} z \in (A \cdot_{𝑜} B) \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset)$
128	127	adantr	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to (A \cdot_{𝑜} z \in (A \cdot_{𝑜} B) \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset)$
129	123 128	syld	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to (z \in B \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset)$
130	129	adantll	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to (z \in B \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset)$
131	121 130	jcad	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to (z \in B \to (\emptyset \in (A \cdot_{𝑜} x) \land A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset))$
132		oveq2	$⊢ w = \emptyset \to (A \cdot_{𝑜} B) +_{𝑜} w = (A \cdot_{𝑜} B) +_{𝑜} \emptyset$
133	132	sseq2d	$⊢ w = \emptyset \to (A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w \leftrightarrow A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset)$
134	133	rspcev	$⊢ (\emptyset \in (A \cdot_{𝑜} x) \land A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} \emptyset) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w$
135	131 134	syl6	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to (z \in B \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
136	135	adantrr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to (z \in B \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
137		omordi	$⊢ ((x \in On \land A \in On) \land \emptyset \in A) \to (v \in x \to A \cdot_{𝑜} v \in (A \cdot_{𝑜} x))$
138	61 137	sylanl1	$⊢ ((Lim x \land A \in On) \land \emptyset \in A) \to (v \in x \to A \cdot_{𝑜} v \in (A \cdot_{𝑜} x))$
139	138	adantrd	$⊢ ((Lim x \land A \in On) \land \emptyset \in A) \to ((v \in x \land B +_{𝑜} v = z) \to A \cdot_{𝑜} v \in (A \cdot_{𝑜} x))$
140	139	adantrr	$⊢ ((Lim x \land A \in On) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ((v \in x \land B +_{𝑜} v = z) \to A \cdot_{𝑜} v \in (A \cdot_{𝑜} x))$
141		oveq2	$⊢ y = v \to B +_{𝑜} y = B +_{𝑜} v$
142	141	oveq2d	$⊢ y = v \to A \cdot_{𝑜} (B +_{𝑜} y) = A \cdot_{𝑜} (B +_{𝑜} v)$
143		oveq2	$⊢ y = v \to A \cdot_{𝑜} y = A \cdot_{𝑜} v$
144	143	oveq2d	$⊢ y = v \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)$
145	142 144	eqeq12d	$⊢ y = v \to (A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \leftrightarrow A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
146	145	rspccv	$⊢ \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to (v \in x \to A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
147		oveq2	$⊢ B +_{𝑜} v = z \to A \cdot_{𝑜} (B +_{𝑜} v) = A \cdot_{𝑜} z$
148		eqeq1	$⊢ A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} (B +_{𝑜} v) = A \cdot_{𝑜} z \leftrightarrow (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v) = A \cdot_{𝑜} z)$
149	147 148	syl5ib	$⊢ A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v) \to (B +_{𝑜} v = z \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v) = A \cdot_{𝑜} z)$
150		eqimss2	$⊢ (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v) = A \cdot_{𝑜} z \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)$
151	149 150	syl6	$⊢ A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v) \to (B +_{𝑜} v = z \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
152	151	imim2i	$⊢ (v \in x \to A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)) \to (v \in x \to (B +_{𝑜} v = z \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
153	152	impd	$⊢ (v \in x \to A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)) \to ((v \in x \land B +_{𝑜} v = z) \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
154	146 153	syl	$⊢ \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to ((v \in x \land B +_{𝑜} v = z) \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
155	154	ad2antll	$⊢ ((Lim x \land A \in On) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ((v \in x \land B +_{𝑜} v = z) \to A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
156	140 155	jcad	$⊢ ((Lim x \land A \in On) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ((v \in x \land B +_{𝑜} v = z) \to (A \cdot_{𝑜} v \in (A \cdot_{𝑜} x) \land A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
157		oveq2	$⊢ w = A \cdot_{𝑜} v \to (A \cdot_{𝑜} B) +_{𝑜} w = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)$
158	157	sseq2d	$⊢ w = A \cdot_{𝑜} v \to (A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w \leftrightarrow A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v))$
159	158	rspcev	$⊢ (A \cdot_{𝑜} v \in (A \cdot_{𝑜} x) \land A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w$
160	156 159	syl6	$⊢ ((Lim x \land A \in On) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ((v \in x \land B +_{𝑜} v = z) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
161	160	rexlimdvw	$⊢ ((Lim x \land A \in On) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to (\exists v \in On (v \in x \land B +_{𝑜} v = z) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
162	161	adantlrr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to (\exists v \in On (v \in x \land B +_{𝑜} v = z) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
163	136 162	jaod	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ((z \in B \lor \exists v \in On (v \in x \land B +_{𝑜} v = z)) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
164	163	adantr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \land z \in (B +_{𝑜} x)) \to ((z \in B \lor \exists v \in On (v \in x \land B +_{𝑜} v = z)) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w)$
165	110 164	mpd	$⊢ (((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \land z \in (B +_{𝑜} x)) \to \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w$
166	165	ralrimiva	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to \forall z \in (B +_{𝑜} x) \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w$
167		iunss2	$⊢ \forall z \in (B +_{𝑜} x) \exists w \in (A \cdot_{𝑜} x) A \cdot_{𝑜} z \subseteq (A \cdot_{𝑜} B) +_{𝑜} w \to ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z) \subseteq ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w)$
168	166 167	syl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z) \subseteq ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w)$
169		omordlim	$⊢ ((A \in On \land (x \in V \land Lim x)) \land w \in (A \cdot_{𝑜} x)) \to \exists v \in x w \in (A \cdot_{𝑜} v)$
170	169	ex	$⊢ (A \in On \land (x \in V \land Lim x)) \to (w \in (A \cdot_{𝑜} x) \to \exists v \in x w \in (A \cdot_{𝑜} v))$
171	59 170	mpanr1	$⊢ (A \in On \land Lim x) \to (w \in (A \cdot_{𝑜} x) \to \exists v \in x w \in (A \cdot_{𝑜} v))$
172	171	ancoms	$⊢ (Lim x \land A \in On) \to (w \in (A \cdot_{𝑜} x) \to \exists v \in x w \in (A \cdot_{𝑜} v))$
173	172	imp	$⊢ ((Lim x \land A \in On) \land w \in (A \cdot_{𝑜} x)) \to \exists v \in x w \in (A \cdot_{𝑜} v)$
174	173	adantlrr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land w \in (A \cdot_{𝑜} x)) \to \exists v \in x w \in (A \cdot_{𝑜} v)$
175	174	adantlr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land w \in (A \cdot_{𝑜} x)) \to \exists v \in x w \in (A \cdot_{𝑜} v)$
176		oaordi	$⊢ (x \in On \land B \in On) \to (v \in x \to B +_{𝑜} v \in (B +_{𝑜} x))$
177	61 176	sylan	$⊢ (Lim x \land B \in On) \to (v \in x \to B +_{𝑜} v \in (B +_{𝑜} x))$
178	177	imp	$⊢ ((Lim x \land B \in On) \land v \in x) \to B +_{𝑜} v \in (B +_{𝑜} x)$
179	178	adantlrl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land v \in x) \to B +_{𝑜} v \in (B +_{𝑜} x)$
180	179	a1d	$⊢ ((Lim x \land (A \in On \land B \in On)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to B +_{𝑜} v \in (B +_{𝑜} x))$
181	180	adantlr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to B +_{𝑜} v \in (B +_{𝑜} x))$
182		limord	$⊢ Lim x \to Ord x$
183		ordelon	$⊢ (Ord x \land v \in x) \to v \in On$
184	182 183	sylan	$⊢ (Lim x \land v \in x) \to v \in On$
185		omcl	$⊢ (A \in On \land v \in On) \to A \cdot_{𝑜} v \in On$
186	185	ancoms	$⊢ (v \in On \land A \in On) \to A \cdot_{𝑜} v \in On$
187	186	adantrr	$⊢ (v \in On \land (A \in On \land B \in On)) \to A \cdot_{𝑜} v \in On$
188	21	adantl	$⊢ (v \in On \land (A \in On \land B \in On)) \to A \cdot_{𝑜} B \in On$
189		oaordi	$⊢ (A \cdot_{𝑜} v \in On \land A \cdot_{𝑜} B \in On) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
190	187 188 189	syl2anc	$⊢ (v \in On \land (A \in On \land B \in On)) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
191	184 190	sylan	$⊢ ((Lim x \land v \in x) \land (A \in On \land B \in On)) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
192	191	an32s	$⊢ ((Lim x \land (A \in On \land B \in On)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
193	192	adantlr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
194	145	rspccva	$⊢ (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \land v \in x) \to A \cdot_{𝑜} (B +_{𝑜} v) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)$
195	194	eleq2d	$⊢ (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \land v \in x) \to ((A \cdot_{𝑜} B) +_{𝑜} w \in (A \cdot_{𝑜} (B +_{𝑜} v)) \leftrightarrow (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
196	195	adantll	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to ((A \cdot_{𝑜} B) +_{𝑜} w \in (A \cdot_{𝑜} (B +_{𝑜} v)) \leftrightarrow (A \cdot_{𝑜} B) +_{𝑜} w \in ((A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} v)))$
197	193 196	sylibrd	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \in (A \cdot_{𝑜} (B +_{𝑜} v)))$
198		oacl	$⊢ (B \in On \land v \in On) \to B +_{𝑜} v \in On$
199	198	ancoms	$⊢ (v \in On \land B \in On) \to B +_{𝑜} v \in On$
200		omcl	$⊢ (A \in On \land B +_{𝑜} v \in On) \to A \cdot_{𝑜} (B +_{𝑜} v) \in On$
201	199 200	sylan2	$⊢ (A \in On \land (v \in On \land B \in On)) \to A \cdot_{𝑜} (B +_{𝑜} v) \in On$
202	201	an12s	$⊢ (v \in On \land (A \in On \land B \in On)) \to A \cdot_{𝑜} (B +_{𝑜} v) \in On$
203	184 202	sylan	$⊢ ((Lim x \land v \in x) \land (A \in On \land B \in On)) \to A \cdot_{𝑜} (B +_{𝑜} v) \in On$
204	203	an32s	$⊢ ((Lim x \land (A \in On \land B \in On)) \land v \in x) \to A \cdot_{𝑜} (B +_{𝑜} v) \in On$
205		onelss	$⊢ A \cdot_{𝑜} (B +_{𝑜} v) \in On \to ((A \cdot_{𝑜} B) +_{𝑜} w \in (A \cdot_{𝑜} (B +_{𝑜} v)) \to (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v))$
206	204 205	syl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land v \in x) \to ((A \cdot_{𝑜} B) +_{𝑜} w \in (A \cdot_{𝑜} (B +_{𝑜} v)) \to (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v))$
207	206	adantlr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to ((A \cdot_{𝑜} B) +_{𝑜} w \in (A \cdot_{𝑜} (B +_{𝑜} v)) \to (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v))$
208	197 207	syld	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v))$
209	181 208	jcad	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to (B +_{𝑜} v \in (B +_{𝑜} x) \land (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v)))$
210		oveq2	$⊢ z = B +_{𝑜} v \to A \cdot_{𝑜} z = A \cdot_{𝑜} (B +_{𝑜} v)$
211	210	sseq2d	$⊢ z = B +_{𝑜} v \to ((A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z \leftrightarrow (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v))$
212	211	rspcev	$⊢ (B +_{𝑜} v \in (B +_{𝑜} x) \land (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} (B +_{𝑜} v)) \to \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z$
213	209 212	syl6	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land v \in x) \to (w \in (A \cdot_{𝑜} v) \to \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z)$
214	213	rexlimdva	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \to (\exists v \in x w \in (A \cdot_{𝑜} v) \to \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z)$
215	214	adantr	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land w \in (A \cdot_{𝑜} x)) \to (\exists v \in x w \in (A \cdot_{𝑜} v) \to \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z)$
216	175 215	mpd	$⊢ (((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \land w \in (A \cdot_{𝑜} x)) \to \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z$
217	216	ralrimiva	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \to \forall w \in (A \cdot_{𝑜} x) \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z$
218		iunss2	$⊢ \forall w \in (A \cdot_{𝑜} x) \exists z \in (B +_{𝑜} x) (A \cdot_{𝑜} B) +_{𝑜} w \subseteq A \cdot_{𝑜} z \to ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w) \subseteq ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
219	217 218	syl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y)) \to ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w) \subseteq ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
220	219	adantrl	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w) \subseteq ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
221	168 220	eqssd	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z) = ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w)$
222		oalimcl	$⊢ (B \in On \land (x \in V \land Lim x)) \to Lim (B +_{𝑜} x)$
223	59 222	mpanr1	$⊢ (B \in On \land Lim x) \to Lim (B +_{𝑜} x)$
224	223	ancoms	$⊢ (Lim x \land B \in On) \to Lim (B +_{𝑜} x)$
225	224	anim2i	$⊢ (A \in On \land (Lim x \land B \in On)) \to (A \in On \land Lim (B +_{𝑜} x))$
226	225	an12s	$⊢ (Lim x \land (A \in On \land B \in On)) \to (A \in On \land Lim (B +_{𝑜} x))$
227		ovex	$⊢ B +_{𝑜} x \in V$
228		omlim	$⊢ (A \in On \land (B +_{𝑜} x \in V \land Lim (B +_{𝑜} x))) \to A \cdot_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
229	227 228	mpanr1	$⊢ (A \in On \land Lim (B +_{𝑜} x)) \to A \cdot_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
230	226 229	syl	$⊢ (Lim x \land (A \in On \land B \in On)) \to A \cdot_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
231	230	adantr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to A \cdot_{𝑜} (B +_{𝑜} x) = ⋃_{z \in B +_{𝑜} x} (A \cdot_{𝑜} z)$
232	21	ad2antlr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to A \cdot_{𝑜} B \in On$
233	59	jctl	$⊢ Lim x \to (x \in V \land Lim x)$
234	233	anim1ci	$⊢ (Lim x \land A \in On) \to (A \in On \land (x \in V \land Lim x))$
235		omlimcl	$⊢ ((A \in On \land (x \in V \land Lim x)) \land \emptyset \in A) \to Lim (A \cdot_{𝑜} x)$
236	234 235	sylan	$⊢ ((Lim x \land A \in On) \land \emptyset \in A) \to Lim (A \cdot_{𝑜} x)$
237	236	adantlrr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to Lim (A \cdot_{𝑜} x)$
238		ovex	$⊢ A \cdot_{𝑜} x \in V$
239	237 238	jctil	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to (A \cdot_{𝑜} x \in V \land Lim (A \cdot_{𝑜} x))$
240		oalim	$⊢ (A \cdot_{𝑜} B \in On \land (A \cdot_{𝑜} x \in V \land Lim (A \cdot_{𝑜} x))) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w)$
241	232 239 240	syl2anc	$⊢ ((Lim x \land (A \in On \land B \in On)) \land \emptyset \in A) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w)$
242	241	adantrr	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x) = ⋃_{w \in A \cdot_{𝑜} x} ((A \cdot_{𝑜} B) +_{𝑜} w)$
243	221 231 242	3eqtr4d	$⊢ ((Lim x \land (A \in On \land B \in On)) \land (\emptyset \in A \land \forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y))) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)$
244	243	exp43	$⊢ Lim x \to ((A \in On \land B \in On) \to (\emptyset \in A \to (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x))))$
245	244	com3l	$⊢ (A \in On \land B \in On) \to (\emptyset \in A \to (Lim x \to (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x))))$
246	245	imp	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to (Lim x \to (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)))$
247	84 246	oe0lem	$⊢ (A \in On \land B \in On) \to (Lim x \to (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)))$
248	247	com12	$⊢ Lim x \to ((A \in On \land B \in On) \to (\forall y \in x A \cdot_{𝑜} (B +_{𝑜} y) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} y) \to A \cdot_{𝑜} (B +_{𝑜} x) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} x)))$
249	5 10 15 20 30 58 248	tfinds3	$⊢ C \in On \to ((A \in On \land B \in On) \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C))$
250	249	expdcom	$⊢ A \in On \to (B \in On \to (C \in On \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)))$
251	250	3imp	$⊢ (A \in On \land B \in On \land C \in On) \to A \cdot_{𝑜} (B +_{𝑜} C) = (A \cdot_{𝑜} B) +_{𝑜} (A \cdot_{𝑜} C)$

Metamath Proof Explorer

Theorem odi

Proof