oeoalem

	Ref	Expression
Hypotheses	oeoalem.1	$⊢ A \in On$
	oeoalem.2	$⊢ \emptyset \in A$
	oeoalem.3	$⊢ B \in On$
Assertion	oeoalem	$⊢ C \in On \to A ↑_{𝑜} (B +_{𝑜} C) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} C)$

Proof

Step	Hyp	Ref	Expression
1		oeoalem.1	$⊢ A \in On$
2		oeoalem.2	$⊢ \emptyset \in A$
3		oeoalem.3	$⊢ B \in On$
4		oveq2	$⊢ x = \emptyset \to B +_{𝑜} x = B +_{𝑜} \emptyset$
5	4	oveq2d	$⊢ x = \emptyset \to A ↑_{𝑜} (B +_{𝑜} x) = A ↑_{𝑜} (B +_{𝑜} \emptyset)$
6		oveq2	$⊢ x = \emptyset \to A ↑_{𝑜} x = A ↑_{𝑜} \emptyset$
7	6	oveq2d	$⊢ x = \emptyset \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} \emptyset)$
8	5 7	eqeq12d	$⊢ x = \emptyset \to (A ↑_{𝑜} (B +_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) \leftrightarrow A ↑_{𝑜} (B +_{𝑜} \emptyset) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} \emptyset))$
9		oveq2	$⊢ x = y \to B +_{𝑜} x = B +_{𝑜} y$
10	9	oveq2d	$⊢ x = y \to A ↑_{𝑜} (B +_{𝑜} x) = A ↑_{𝑜} (B +_{𝑜} y)$
11		oveq2	$⊢ x = y \to A ↑_{𝑜} x = A ↑_{𝑜} y$
12	11	oveq2d	$⊢ x = y \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)$
13	10 12	eqeq12d	$⊢ x = y \to (A ↑_{𝑜} (B +_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) \leftrightarrow A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
14		oveq2	$⊢ x = suc y \to B +_{𝑜} x = B +_{𝑜} suc y$
15	14	oveq2d	$⊢ x = suc y \to A ↑_{𝑜} (B +_{𝑜} x) = A ↑_{𝑜} (B +_{𝑜} suc y)$
16		oveq2	$⊢ x = suc y \to A ↑_{𝑜} x = A ↑_{𝑜} suc y$
17	16	oveq2d	$⊢ x = suc y \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y)$
18	15 17	eqeq12d	$⊢ x = suc y \to (A ↑_{𝑜} (B +_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) \leftrightarrow A ↑_{𝑜} (B +_{𝑜} suc y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y))$
19		oveq2	$⊢ x = C \to B +_{𝑜} x = B +_{𝑜} C$
20	19	oveq2d	$⊢ x = C \to A ↑_{𝑜} (B +_{𝑜} x) = A ↑_{𝑜} (B +_{𝑜} C)$
21		oveq2	$⊢ x = C \to A ↑_{𝑜} x = A ↑_{𝑜} C$
22	21	oveq2d	$⊢ x = C \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} C)$
23	20 22	eqeq12d	$⊢ x = C \to (A ↑_{𝑜} (B +_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) \leftrightarrow A ↑_{𝑜} (B +_{𝑜} C) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} C))$
24		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
25	1 3 24	mp2an	$⊢ A ↑_{𝑜} B \in On$
26		om1	$⊢ A ↑_{𝑜} B \in On \to (A ↑_{𝑜} B) \cdot_{𝑜} 1_{𝑜} = A ↑_{𝑜} B$
27	25 26	ax-mp	$⊢ (A ↑_{𝑜} B) \cdot_{𝑜} 1_{𝑜} = A ↑_{𝑜} B$
28		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
29	1 28	ax-mp	$⊢ A ↑_{𝑜} \emptyset = 1_{𝑜}$
30	29	oveq2i	$⊢ (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} \emptyset) = (A ↑_{𝑜} B) \cdot_{𝑜} 1_{𝑜}$
31		oa0	$⊢ B \in On \to B +_{𝑜} \emptyset = B$
32	3 31	ax-mp	$⊢ B +_{𝑜} \emptyset = B$
33	32	oveq2i	$⊢ A ↑_{𝑜} (B +_{𝑜} \emptyset) = A ↑_{𝑜} B$
34	27 30 33	3eqtr4ri	$⊢ A ↑_{𝑜} (B +_{𝑜} \emptyset) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} \emptyset)$
35		oasuc	$⊢ (B \in On \land y \in On) \to B +_{𝑜} suc y = suc (B +_{𝑜} y)$
36	35	oveq2d	$⊢ (B \in On \land y \in On) \to A ↑_{𝑜} (B +_{𝑜} suc y) = A ↑_{𝑜} suc (B +_{𝑜} y)$
37		oacl	$⊢ (B \in On \land y \in On) \to B +_{𝑜} y \in On$
38		oesuc	$⊢ (A \in On \land B +_{𝑜} y \in On) \to A ↑_{𝑜} suc (B +_{𝑜} y) = (A ↑_{𝑜} (B +_{𝑜} y)) \cdot_{𝑜} A$
39	1 37 38	sylancr	$⊢ (B \in On \land y \in On) \to A ↑_{𝑜} suc (B +_{𝑜} y) = (A ↑_{𝑜} (B +_{𝑜} y)) \cdot_{𝑜} A$
40	36 39	eqtrd	$⊢ (B \in On \land y \in On) \to A ↑_{𝑜} (B +_{𝑜} suc y) = (A ↑_{𝑜} (B +_{𝑜} y)) \cdot_{𝑜} A$
41	3 40	mpan	$⊢ y \in On \to A ↑_{𝑜} (B +_{𝑜} suc y) = (A ↑_{𝑜} (B +_{𝑜} y)) \cdot_{𝑜} A$
42		oveq1	$⊢ A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y) \to (A ↑_{𝑜} (B +_{𝑜} y)) \cdot_{𝑜} A = ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A$
43	41 42	sylan9eq	$⊢ (y \in On \land A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \to A ↑_{𝑜} (B +_{𝑜} suc y) = ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A$
44		oecl	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} y \in On$
45		omass	$⊢ (A ↑_{𝑜} B \in On \land A ↑_{𝑜} y \in On \land A \in On) \to ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A = (A ↑_{𝑜} B) \cdot_{𝑜} ((A ↑_{𝑜} y) \cdot_{𝑜} A)$
46	25 1 45	mp3an13	$⊢ A ↑_{𝑜} y \in On \to ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A = (A ↑_{𝑜} B) \cdot_{𝑜} ((A ↑_{𝑜} y) \cdot_{𝑜} A)$
47	44 46	syl	$⊢ (A \in On \land y \in On) \to ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A = (A ↑_{𝑜} B) \cdot_{𝑜} ((A ↑_{𝑜} y) \cdot_{𝑜} A)$
48		oesuc	$⊢ (A \in On \land y \in On) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
49	48	oveq2d	$⊢ (A \in On \land y \in On) \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y) = (A ↑_{𝑜} B) \cdot_{𝑜} ((A ↑_{𝑜} y) \cdot_{𝑜} A)$
50	47 49	eqtr4d	$⊢ (A \in On \land y \in On) \to ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y)$
51	1 50	mpan	$⊢ y \in On \to ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y)$
52	51	adantr	$⊢ (y \in On \land A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \to ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \cdot_{𝑜} A = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y)$
53	43 52	eqtrd	$⊢ (y \in On \land A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \to A ↑_{𝑜} (B +_{𝑜} suc y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y)$
54	53	ex	$⊢ y \in On \to (A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y) \to A ↑_{𝑜} (B +_{𝑜} suc y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} suc y))$
55		vex	$⊢ x \in V$
56		oalim	$⊢ (B \in On \land (x \in V \land Lim x)) \to B +_{𝑜} x = ⋃_{y \in x} (B +_{𝑜} y)$
57	3 56	mpan	$⊢ (x \in V \land Lim x) \to B +_{𝑜} x = ⋃_{y \in x} (B +_{𝑜} y)$
58	55 57	mpan	$⊢ Lim x \to B +_{𝑜} x = ⋃_{y \in x} (B +_{𝑜} y)$
59	58	oveq2d	$⊢ Lim x \to A ↑_{𝑜} (B +_{𝑜} x) = A ↑_{𝑜} ⋃_{y \in x} (B +_{𝑜} y)$
60		limord	$⊢ Lim x \to Ord x$
61		ordelon	$⊢ (Ord x \land y \in x) \to y \in On$
62	60 61	sylan	$⊢ (Lim x \land y \in x) \to y \in On$
63	3 62 37	sylancr	$⊢ (Lim x \land y \in x) \to B +_{𝑜} y \in On$
64	63	ralrimiva	$⊢ Lim x \to \forall y \in x B +_{𝑜} y \in On$
65		0ellim	$⊢ Lim x \to \emptyset \in x$
66	65	ne0d	$⊢ Lim x \to x \neq \emptyset$
67		vex	$⊢ w \in V$
68		oelim	$⊢ ((A \in On \land (w \in V \land Lim w)) \land \emptyset \in A) \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
69	2 68	mpan2	$⊢ (A \in On \land (w \in V \land Lim w)) \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
70	1 69	mpan	$⊢ (w \in V \land Lim w) \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
71	67 70	mpan	$⊢ Lim w \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
72		oewordi	$⊢ ((z \in On \land w \in On \land A \in On) \land \emptyset \in A) \to (z \subseteq w \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w)$
73	2 72	mpan2	$⊢ (z \in On \land w \in On \land A \in On) \to (z \subseteq w \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w)$
74	1 73	mp3an3	$⊢ (z \in On \land w \in On) \to (z \subseteq w \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w)$
75	74	3impia	$⊢ (z \in On \land w \in On \land z \subseteq w) \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w$
76	71 75	onoviun	$⊢ (x \in V \land \forall y \in x B +_{𝑜} y \in On \land x \neq \emptyset) \to A ↑_{𝑜} ⋃_{y \in x} (B +_{𝑜} y) = ⋃_{y \in x} (A ↑_{𝑜} (B +_{𝑜} y))$
77	55 64 66 76	mp3an2i	$⊢ Lim x \to A ↑_{𝑜} ⋃_{y \in x} (B +_{𝑜} y) = ⋃_{y \in x} (A ↑_{𝑜} (B +_{𝑜} y))$
78	59 77	eqtrd	$⊢ Lim x \to A ↑_{𝑜} (B +_{𝑜} x) = ⋃_{y \in x} (A ↑_{𝑜} (B +_{𝑜} y))$
79		iuneq2	$⊢ \forall y \in x A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y) \to ⋃_{y \in x} (A ↑_{𝑜} (B +_{𝑜} y)) = ⋃_{y \in x} ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
80	78 79	sylan9eq	$⊢ (Lim x \land \forall y \in x A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \to A ↑_{𝑜} (B +_{𝑜} x) = ⋃_{y \in x} ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
81		oelim	$⊢ ((A \in On \land (x \in V \land Lim x)) \land \emptyset \in A) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
82	2 81	mpan2	$⊢ (A \in On \land (x \in V \land Lim x)) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
83	1 82	mpan	$⊢ (x \in V \land Lim x) \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
84	55 83	mpan	$⊢ Lim x \to A ↑_{𝑜} x = ⋃_{y \in x} (A ↑_{𝑜} y)$
85	84	oveq2d	$⊢ Lim x \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} ⋃_{y \in x} (A ↑_{𝑜} y)$
86	1 62 44	sylancr	$⊢ (Lim x \land y \in x) \to A ↑_{𝑜} y \in On$
87	86	ralrimiva	$⊢ Lim x \to \forall y \in x A ↑_{𝑜} y \in On$
88		omlim	$⊢ (A ↑_{𝑜} B \in On \land (w \in V \land Lim w)) \to (A ↑_{𝑜} B) \cdot_{𝑜} w = ⋃_{z \in w} ((A ↑_{𝑜} B) \cdot_{𝑜} z)$
89	25 88	mpan	$⊢ (w \in V \land Lim w) \to (A ↑_{𝑜} B) \cdot_{𝑜} w = ⋃_{z \in w} ((A ↑_{𝑜} B) \cdot_{𝑜} z)$
90	67 89	mpan	$⊢ Lim w \to (A ↑_{𝑜} B) \cdot_{𝑜} w = ⋃_{z \in w} ((A ↑_{𝑜} B) \cdot_{𝑜} z)$
91		omwordi	$⊢ (z \in On \land w \in On \land A ↑_{𝑜} B \in On) \to (z \subseteq w \to (A ↑_{𝑜} B) \cdot_{𝑜} z \subseteq (A ↑_{𝑜} B) \cdot_{𝑜} w)$
92	25 91	mp3an3	$⊢ (z \in On \land w \in On) \to (z \subseteq w \to (A ↑_{𝑜} B) \cdot_{𝑜} z \subseteq (A ↑_{𝑜} B) \cdot_{𝑜} w)$
93	92	3impia	$⊢ (z \in On \land w \in On \land z \subseteq w) \to (A ↑_{𝑜} B) \cdot_{𝑜} z \subseteq (A ↑_{𝑜} B) \cdot_{𝑜} w$
94	90 93	onoviun	$⊢ (x \in V \land \forall y \in x A ↑_{𝑜} y \in On \land x \neq \emptyset) \to (A ↑_{𝑜} B) \cdot_{𝑜} ⋃_{y \in x} (A ↑_{𝑜} y) = ⋃_{y \in x} ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
95	55 87 66 94	mp3an2i	$⊢ Lim x \to (A ↑_{𝑜} B) \cdot_{𝑜} ⋃_{y \in x} (A ↑_{𝑜} y) = ⋃_{y \in x} ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
96	85 95	eqtrd	$⊢ Lim x \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = ⋃_{y \in x} ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
97	96	adantr	$⊢ (Lim x \land \forall y \in x A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \to (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x) = ⋃_{y \in x} ((A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y))$
98	80 97	eqtr4d	$⊢ (Lim x \land \forall y \in x A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y)) \to A ↑_{𝑜} (B +_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x)$
99	98	ex	$⊢ Lim x \to (\forall y \in x A ↑_{𝑜} (B +_{𝑜} y) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} y) \to A ↑_{𝑜} (B +_{𝑜} x) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} x))$
100	8 13 18 23 34 54 99	tfinds	$⊢ C \in On \to A ↑_{𝑜} (B +_{𝑜} C) = (A ↑_{𝑜} B) \cdot_{𝑜} (A ↑_{𝑜} C)$

Metamath Proof Explorer

Theorem oeoalem

Proof