oeoelem

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

Proof

Step	Hyp	Ref	Expression
1		oeoelem.1	$⊢ A \in On$
2		oeoelem.2	$⊢ \emptyset \in A$
3		oveq2	$⊢ x = \emptyset \to (A ↑_{𝑜} B) ↑_{𝑜} x = (A ↑_{𝑜} B) ↑_{𝑜} \emptyset$
4		oveq2	$⊢ x = \emptyset \to B \cdot_{𝑜} x = B \cdot_{𝑜} \emptyset$
5	4	oveq2d	$⊢ x = \emptyset \to A ↑_{𝑜} (B \cdot_{𝑜} x) = A ↑_{𝑜} (B \cdot_{𝑜} \emptyset)$
6	3 5	eqeq12d	$⊢ x = \emptyset \to ((A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x) \leftrightarrow (A ↑_{𝑜} B) ↑_{𝑜} \emptyset = A ↑_{𝑜} (B \cdot_{𝑜} \emptyset))$
7		oveq2	$⊢ x = y \to (A ↑_{𝑜} B) ↑_{𝑜} x = (A ↑_{𝑜} B) ↑_{𝑜} y$
8		oveq2	$⊢ x = y \to B \cdot_{𝑜} x = B \cdot_{𝑜} y$
9	8	oveq2d	$⊢ x = y \to A ↑_{𝑜} (B \cdot_{𝑜} x) = A ↑_{𝑜} (B \cdot_{𝑜} y)$
10	7 9	eqeq12d	$⊢ x = y \to ((A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x) \leftrightarrow (A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y))$
11		oveq2	$⊢ x = suc y \to (A ↑_{𝑜} B) ↑_{𝑜} x = (A ↑_{𝑜} B) ↑_{𝑜} suc y$
12		oveq2	$⊢ x = suc y \to B \cdot_{𝑜} x = B \cdot_{𝑜} suc y$
13	12	oveq2d	$⊢ x = suc y \to A ↑_{𝑜} (B \cdot_{𝑜} x) = A ↑_{𝑜} (B \cdot_{𝑜} suc y)$
14	11 13	eqeq12d	$⊢ x = suc y \to ((A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x) \leftrightarrow (A ↑_{𝑜} B) ↑_{𝑜} suc y = A ↑_{𝑜} (B \cdot_{𝑜} suc y))$
15		oveq2	$⊢ x = C \to (A ↑_{𝑜} B) ↑_{𝑜} x = (A ↑_{𝑜} B) ↑_{𝑜} C$
16		oveq2	$⊢ x = C \to B \cdot_{𝑜} x = B \cdot_{𝑜} C$
17	16	oveq2d	$⊢ x = C \to A ↑_{𝑜} (B \cdot_{𝑜} x) = A ↑_{𝑜} (B \cdot_{𝑜} C)$
18	15 17	eqeq12d	$⊢ x = C \to ((A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x) \leftrightarrow (A ↑_{𝑜} B) ↑_{𝑜} C = A ↑_{𝑜} (B \cdot_{𝑜} C))$
19		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
20	1 19	mpan	$⊢ B \in On \to A ↑_{𝑜} B \in On$
21		oe0	$⊢ A ↑_{𝑜} B \in On \to (A ↑_{𝑜} B) ↑_{𝑜} \emptyset = 1_{𝑜}$
22	20 21	syl	$⊢ B \in On \to (A ↑_{𝑜} B) ↑_{𝑜} \emptyset = 1_{𝑜}$
23		om0	$⊢ B \in On \to B \cdot_{𝑜} \emptyset = \emptyset$
24	23	oveq2d	$⊢ B \in On \to A ↑_{𝑜} (B \cdot_{𝑜} \emptyset) = A ↑_{𝑜} \emptyset$
25		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
26	1 25	ax-mp	$⊢ A ↑_{𝑜} \emptyset = 1_{𝑜}$
27	24 26	eqtrdi	$⊢ B \in On \to A ↑_{𝑜} (B \cdot_{𝑜} \emptyset) = 1_{𝑜}$
28	22 27	eqtr4d	$⊢ B \in On \to (A ↑_{𝑜} B) ↑_{𝑜} \emptyset = A ↑_{𝑜} (B \cdot_{𝑜} \emptyset)$
29		oveq1	$⊢ (A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y) \to ((A ↑_{𝑜} B) ↑_{𝑜} y) \cdot_{𝑜} (A ↑_{𝑜} B) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B)$
30		oesuc	$⊢ (A ↑_{𝑜} B \in On \land y \in On) \to (A ↑_{𝑜} B) ↑_{𝑜} suc y = ((A ↑_{𝑜} B) ↑_{𝑜} y) \cdot_{𝑜} (A ↑_{𝑜} B)$
31	20 30	sylan	$⊢ (B \in On \land y \in On) \to (A ↑_{𝑜} B) ↑_{𝑜} suc y = ((A ↑_{𝑜} B) ↑_{𝑜} y) \cdot_{𝑜} (A ↑_{𝑜} B)$
32		omsuc	$⊢ (B \in On \land y \in On) \to B \cdot_{𝑜} suc y = (B \cdot_{𝑜} y) +_{𝑜} B$
33	32	oveq2d	$⊢ (B \in On \land y \in On) \to A ↑_{𝑜} (B \cdot_{𝑜} suc y) = A ↑_{𝑜} ((B \cdot_{𝑜} y) +_{𝑜} B)$
34		omcl	$⊢ (B \in On \land y \in On) \to B \cdot_{𝑜} y \in On$
35		oeoa	$⊢ (A \in On \land B \cdot_{𝑜} y \in On \land B \in On) \to A ↑_{𝑜} ((B \cdot_{𝑜} y) +_{𝑜} B) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B)$
36	1 35	mp3an1	$⊢ (B \cdot_{𝑜} y \in On \land B \in On) \to A ↑_{𝑜} ((B \cdot_{𝑜} y) +_{𝑜} B) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B)$
37	34 36	sylan	$⊢ ((B \in On \land y \in On) \land B \in On) \to A ↑_{𝑜} ((B \cdot_{𝑜} y) +_{𝑜} B) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B)$
38	37	anabss1	$⊢ (B \in On \land y \in On) \to A ↑_{𝑜} ((B \cdot_{𝑜} y) +_{𝑜} B) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B)$
39	33 38	eqtrd	$⊢ (B \in On \land y \in On) \to A ↑_{𝑜} (B \cdot_{𝑜} suc y) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B)$
40	31 39	eqeq12d	$⊢ (B \in On \land y \in On) \to ((A ↑_{𝑜} B) ↑_{𝑜} suc y = A ↑_{𝑜} (B \cdot_{𝑜} suc y) \leftrightarrow ((A ↑_{𝑜} B) ↑_{𝑜} y) \cdot_{𝑜} (A ↑_{𝑜} B) = (A ↑_{𝑜} (B \cdot_{𝑜} y)) \cdot_{𝑜} (A ↑_{𝑜} B))$
41	29 40	imbitrrid	$⊢ (B \in On \land y \in On) \to ((A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y) \to (A ↑_{𝑜} B) ↑_{𝑜} suc y = A ↑_{𝑜} (B \cdot_{𝑜} suc y))$
42	41	expcom	$⊢ y \in On \to (B \in On \to ((A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y) \to (A ↑_{𝑜} B) ↑_{𝑜} suc y = A ↑_{𝑜} (B \cdot_{𝑜} suc y)))$
43		iuneq2	$⊢ \forall y \in x (A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y) \to ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y) = ⋃_{y \in x} (A ↑_{𝑜} (B \cdot_{𝑜} y))$
44		vex	$⊢ x \in V$
45		oen0	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to \emptyset \in (A ↑_{𝑜} B)$
46	2 45	mpan2	$⊢ (A \in On \land B \in On) \to \emptyset \in (A ↑_{𝑜} B)$
47		oelim	$⊢ ((A ↑_{𝑜} B \in On \land (x \in V \land Lim x)) \land \emptyset \in (A ↑_{𝑜} B)) \to (A ↑_{𝑜} B) ↑_{𝑜} x = ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y)$
48	19 47	sylanl1	$⊢ (((A \in On \land B \in On) \land (x \in V \land Lim x)) \land \emptyset \in (A ↑_{𝑜} B)) \to (A ↑_{𝑜} B) ↑_{𝑜} x = ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y)$
49	46 48	mpidan	$⊢ ((A \in On \land B \in On) \land (x \in V \land Lim x)) \to (A ↑_{𝑜} B) ↑_{𝑜} x = ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y)$
50	1 49	mpanl1	$⊢ (B \in On \land (x \in V \land Lim x)) \to (A ↑_{𝑜} B) ↑_{𝑜} x = ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y)$
51	44 50	mpanr1	$⊢ (B \in On \land Lim x) \to (A ↑_{𝑜} B) ↑_{𝑜} x = ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y)$
52		omlim	$⊢ (B \in On \land (x \in V \land Lim x)) \to B \cdot_{𝑜} x = ⋃_{y \in x} (B \cdot_{𝑜} y)$
53	44 52	mpanr1	$⊢ (B \in On \land Lim x) \to B \cdot_{𝑜} x = ⋃_{y \in x} (B \cdot_{𝑜} y)$
54	53	oveq2d	$⊢ (B \in On \land Lim x) \to A ↑_{𝑜} (B \cdot_{𝑜} x) = A ↑_{𝑜} ⋃_{y \in x} (B \cdot_{𝑜} y)$
55		limord	$⊢ Lim x \to Ord x$
56		ordelon	$⊢ (Ord x \land y \in x) \to y \in On$
57	55 56	sylan	$⊢ (Lim x \land y \in x) \to y \in On$
58	57 34	sylan2	$⊢ (B \in On \land (Lim x \land y \in x)) \to B \cdot_{𝑜} y \in On$
59	58	anassrs	$⊢ ((B \in On \land Lim x) \land y \in x) \to B \cdot_{𝑜} y \in On$
60	59	ralrimiva	$⊢ (B \in On \land Lim x) \to \forall y \in x B \cdot_{𝑜} y \in On$
61		0ellim	$⊢ Lim x \to \emptyset \in x$
62	61	ne0d	$⊢ Lim x \to x \neq \emptyset$
63	62	adantl	$⊢ (B \in On \land Lim x) \to x \neq \emptyset$
64		vex	$⊢ w \in V$
65		oelim	$⊢ ((A \in On \land (w \in V \land Lim w)) \land \emptyset \in A) \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
66	2 65	mpan2	$⊢ (A \in On \land (w \in V \land Lim w)) \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
67	1 66	mpan	$⊢ (w \in V \land Lim w) \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
68	64 67	mpan	$⊢ Lim w \to A ↑_{𝑜} w = ⋃_{z \in w} (A ↑_{𝑜} z)$
69		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)$
70	2 69	mpan2	$⊢ (z \in On \land w \in On \land A \in On) \to (z \subseteq w \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w)$
71	1 70	mp3an3	$⊢ (z \in On \land w \in On) \to (z \subseteq w \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w)$
72	71	3impia	$⊢ (z \in On \land w \in On \land z \subseteq w) \to A ↑_{𝑜} z \subseteq A ↑_{𝑜} w$
73	68 72	onoviun	$⊢ (x \in V \land \forall y \in x B \cdot_{𝑜} y \in On \land x \neq \emptyset) \to A ↑_{𝑜} ⋃_{y \in x} (B \cdot_{𝑜} y) = ⋃_{y \in x} (A ↑_{𝑜} (B \cdot_{𝑜} y))$
74	44 60 63 73	mp3an2i	$⊢ (B \in On \land Lim x) \to A ↑_{𝑜} ⋃_{y \in x} (B \cdot_{𝑜} y) = ⋃_{y \in x} (A ↑_{𝑜} (B \cdot_{𝑜} y))$
75	54 74	eqtrd	$⊢ (B \in On \land Lim x) \to A ↑_{𝑜} (B \cdot_{𝑜} x) = ⋃_{y \in x} (A ↑_{𝑜} (B \cdot_{𝑜} y))$
76	51 75	eqeq12d	$⊢ (B \in On \land Lim x) \to ((A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x) \leftrightarrow ⋃_{y \in x} ((A ↑_{𝑜} B) ↑_{𝑜} y) = ⋃_{y \in x} (A ↑_{𝑜} (B \cdot_{𝑜} y)))$
77	43 76	imbitrrid	$⊢ (B \in On \land Lim x) \to (\forall y \in x (A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y) \to (A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x))$
78	77	expcom	$⊢ Lim x \to (B \in On \to (\forall y \in x (A ↑_{𝑜} B) ↑_{𝑜} y = A ↑_{𝑜} (B \cdot_{𝑜} y) \to (A ↑_{𝑜} B) ↑_{𝑜} x = A ↑_{𝑜} (B \cdot_{𝑜} x)))$
79	6 10 14 18 28 42 78	tfinds3	$⊢ C \in On \to (B \in On \to (A ↑_{𝑜} B) ↑_{𝑜} C = A ↑_{𝑜} (B \cdot_{𝑜} C))$
80	79	impcom	$⊢ (B \in On \land C \in On) \to (A ↑_{𝑜} B) ↑_{𝑜} C = A ↑_{𝑜} (B \cdot_{𝑜} C)$

Metamath Proof Explorer

Theorem oeoelem

Proof