omabs

Description: Ordinal multiplication is also absorbed by powers of _om . (Contributed by Mario Carneiro, 30-May-2015)

		Ref	Expression
	Assertion	omabs	$⊢ ((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ x = \emptyset \to (\emptyset \in x \leftrightarrow \emptyset \in \emptyset)$
2		oveq2	$⊢ x = \emptyset \to ω ↑_{𝑜} x = ω ↑_{𝑜} \emptyset$
3	2	oveq2d	$⊢ x = \emptyset \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = A \cdot_{𝑜} (ω ↑_{𝑜} \emptyset)$
4	3 2	eqeq12d	$⊢ x = \emptyset \to (A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} \emptyset) = ω ↑_{𝑜} \emptyset)$
5	1 4	imbi12d	$⊢ x = \emptyset \to ((\emptyset \in x \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x) \leftrightarrow (\emptyset \in \emptyset \to A \cdot_{𝑜} (ω ↑_{𝑜} \emptyset) = ω ↑_{𝑜} \emptyset))$
6		eleq2	$⊢ x = y \to (\emptyset \in x \leftrightarrow \emptyset \in y)$
7		oveq2	$⊢ x = y \to ω ↑_{𝑜} x = ω ↑_{𝑜} y$
8	7	oveq2d	$⊢ x = y \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = A \cdot_{𝑜} (ω ↑_{𝑜} y)$
9	8 7	eqeq12d	$⊢ x = y \to (A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)$
10	6 9	imbi12d	$⊢ x = y \to ((\emptyset \in x \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x) \leftrightarrow (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y))$
11		eleq2	$⊢ x = suc y \to (\emptyset \in x \leftrightarrow \emptyset \in suc y)$
12		oveq2	$⊢ x = suc y \to ω ↑_{𝑜} x = ω ↑_{𝑜} suc y$
13	12	oveq2d	$⊢ x = suc y \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = A \cdot_{𝑜} (ω ↑_{𝑜} suc y)$
14	13 12	eqeq12d	$⊢ x = suc y \to (A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y)$
15	11 14	imbi12d	$⊢ x = suc y \to ((\emptyset \in x \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x) \leftrightarrow (\emptyset \in suc y \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y))$
16		eleq2	$⊢ x = B \to (\emptyset \in x \leftrightarrow \emptyset \in B)$
17		oveq2	$⊢ x = B \to ω ↑_{𝑜} x = ω ↑_{𝑜} B$
18	17	oveq2d	$⊢ x = B \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = A \cdot_{𝑜} (ω ↑_{𝑜} B)$
19	18 17	eqeq12d	$⊢ x = B \to (A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B)$
20	16 19	imbi12d	$⊢ x = B \to ((\emptyset \in x \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x) \leftrightarrow (\emptyset \in B \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B))$
21		noel	$⊢ \neg \emptyset \in \emptyset$
22	21	pm2.21i	$⊢ \emptyset \in \emptyset \to A \cdot_{𝑜} (ω ↑_{𝑜} \emptyset) = ω ↑_{𝑜} \emptyset$
23	22	a1i	$⊢ ((A \in ω \land \emptyset \in A) \land ω \in On) \to (\emptyset \in \emptyset \to A \cdot_{𝑜} (ω ↑_{𝑜} \emptyset) = ω ↑_{𝑜} \emptyset)$
24		simprl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ω \in On$
25		simpll	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to A \in ω$
26		simplr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to \emptyset \in A$
27		omabslem	$⊢ (ω \in On \land A \in ω \land \emptyset \in A) \to A \cdot_{𝑜} ω = ω$
28	24 25 26 27	syl3anc	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to A \cdot_{𝑜} ω = ω$
29	28	adantr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \land y = \emptyset) \to A \cdot_{𝑜} ω = ω$
30		suceq	$⊢ y = \emptyset \to suc y = suc \emptyset$
31		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
32	30 31	eqtr4di	$⊢ y = \emptyset \to suc y = 1_{𝑜}$
33	32	oveq2d	$⊢ y = \emptyset \to ω ↑_{𝑜} suc y = ω ↑_{𝑜} 1_{𝑜}$
34		oe1	$⊢ ω \in On \to ω ↑_{𝑜} 1_{𝑜} = ω$
35	34	ad2antrl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ω ↑_{𝑜} 1_{𝑜} = ω$
36	33 35	sylan9eqr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \land y = \emptyset) \to ω ↑_{𝑜} suc y = ω$
37	36	oveq2d	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \land y = \emptyset) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = A \cdot_{𝑜} ω$
38	29 37 36	3eqtr4d	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \land y = \emptyset) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y$
39	38	ex	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (y = \emptyset \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y)$
40	39	a1dd	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (y = \emptyset \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y))$
41		oveq1	$⊢ A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \to (A \cdot_{𝑜} (ω ↑_{𝑜} y)) \cdot_{𝑜} ω = (ω ↑_{𝑜} y) \cdot_{𝑜} ω$
42		oesuc	$⊢ (ω \in On \land y \in On) \to ω ↑_{𝑜} suc y = (ω ↑_{𝑜} y) \cdot_{𝑜} ω$
43	42	adantl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ω ↑_{𝑜} suc y = (ω ↑_{𝑜} y) \cdot_{𝑜} ω$
44	43	oveq2d	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = A \cdot_{𝑜} ((ω ↑_{𝑜} y) \cdot_{𝑜} ω)$
45		nnon	$⊢ A \in ω \to A \in On$
46	45	ad2antrr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to A \in On$
47		oecl	$⊢ (ω \in On \land y \in On) \to ω ↑_{𝑜} y \in On$
48	47	adantl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ω ↑_{𝑜} y \in On$
49		omass	$⊢ (A \in On \land ω ↑_{𝑜} y \in On \land ω \in On) \to (A \cdot_{𝑜} (ω ↑_{𝑜} y)) \cdot_{𝑜} ω = A \cdot_{𝑜} ((ω ↑_{𝑜} y) \cdot_{𝑜} ω)$
50	46 48 24 49	syl3anc	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (A \cdot_{𝑜} (ω ↑_{𝑜} y)) \cdot_{𝑜} ω = A \cdot_{𝑜} ((ω ↑_{𝑜} y) \cdot_{𝑜} ω)$
51	44 50	eqtr4d	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = (A \cdot_{𝑜} (ω ↑_{𝑜} y)) \cdot_{𝑜} ω$
52	51 43	eqeq12d	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y \leftrightarrow (A \cdot_{𝑜} (ω ↑_{𝑜} y)) \cdot_{𝑜} ω = (ω ↑_{𝑜} y) \cdot_{𝑜} ω)$
53	41 52	imbitrrid	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y)$
54	53	imim2d	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y))$
55	54	com23	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (\emptyset \in y \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y))$
56		simprr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to y \in On$
57		on0eqel	$⊢ y \in On \to (y = \emptyset \lor \emptyset \in y)$
58	56 57	syl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to (y = \emptyset \lor \emptyset \in y)$
59	40 55 58	mpjaod	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y)$
60	59	a1dd	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land y \in On)) \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in suc y \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y))$
61	60	anassrs	$⊢ (((A \in ω \land \emptyset \in A) \land ω \in On) \land y \in On) \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in suc y \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y))$
62	61	expcom	$⊢ y \in On \to (((A \in ω \land \emptyset \in A) \land ω \in On) \to ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in suc y \to A \cdot_{𝑜} (ω ↑_{𝑜} suc y) = ω ↑_{𝑜} suc y)))$
63	45	ad3antrrr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to A \in On$
64		simprl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to ω \in On$
65		simprr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to Lim x$
66		vex	$⊢ x \in V$
67	65 66	jctil	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to (x \in V \land Lim x)$
68		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
69	67 68	syl	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to x \in On$
70		oecl	$⊢ (ω \in On \land x \in On) \to ω ↑_{𝑜} x \in On$
71	64 69 70	syl2anc	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to ω ↑_{𝑜} x \in On$
72	71	adantr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to ω ↑_{𝑜} x \in On$
73		1onn	$⊢ 1_{𝑜} \in ω$
74		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
75	64 73 74	sylanblrc	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to ω \in (On ∖ 2_{𝑜})$
76	75	adantr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to ω \in (On ∖ 2_{𝑜})$
77	67	adantr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (x \in V \land Lim x)$
78		oelimcl	$⊢ (ω \in (On ∖ 2_{𝑜}) \land (x \in V \land Lim x)) \to Lim (ω ↑_{𝑜} x)$
79	76 77 78	syl2anc	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to Lim (ω ↑_{𝑜} x)$
80		omlim	$⊢ (A \in On \land (ω ↑_{𝑜} x \in On \land Lim (ω ↑_{𝑜} x))) \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ⋃_{z \in ω ↑_{𝑜} x} (A \cdot_{𝑜} z)$
81	63 72 79 80	syl12anc	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ⋃_{z \in ω ↑_{𝑜} x} (A \cdot_{𝑜} z)$
82		simplrl	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to ω \in On$
83		oelim2	$⊢ (ω \in On \land (x \in V \land Lim x)) \to ω ↑_{𝑜} x = ⋃_{y \in x ∖ 1_{𝑜}} (ω ↑_{𝑜} y)$
84	82 77 83	syl2anc	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to ω ↑_{𝑜} x = ⋃_{y \in x ∖ 1_{𝑜}} (ω ↑_{𝑜} y)$
85	84	eleq2d	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (z \in (ω ↑_{𝑜} x) \leftrightarrow z \in ⋃_{y \in x ∖ 1_{𝑜}} (ω ↑_{𝑜} y))$
86		eliun	$⊢ z \in ⋃_{y \in x ∖ 1_{𝑜}} (ω ↑_{𝑜} y) \leftrightarrow \exists y \in (x ∖ 1_{𝑜}) z \in (ω ↑_{𝑜} y)$
87	85 86	bitrdi	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (z \in (ω ↑_{𝑜} x) \leftrightarrow \exists y \in (x ∖ 1_{𝑜}) z \in (ω ↑_{𝑜} y))$
88	69	adantr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to x \in On$
89		anass	$⊢ ((y \in x \land \emptyset \in y) \land z \in (ω ↑_{𝑜} y)) \leftrightarrow (y \in x \land (\emptyset \in y \land z \in (ω ↑_{𝑜} y)))$
90		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
91		on0eln0	$⊢ y \in On \to (\emptyset \in y \leftrightarrow y \neq \emptyset)$
92	90 91	syl	$⊢ (x \in On \land y \in x) \to (\emptyset \in y \leftrightarrow y \neq \emptyset)$
93	92	pm5.32da	$⊢ x \in On \to ((y \in x \land \emptyset \in y) \leftrightarrow (y \in x \land y \neq \emptyset))$
94		dif1o	$⊢ y \in (x ∖ 1_{𝑜}) \leftrightarrow (y \in x \land y \neq \emptyset)$
95	93 94	bitr4di	$⊢ x \in On \to ((y \in x \land \emptyset \in y) \leftrightarrow y \in (x ∖ 1_{𝑜}))$
96	95	anbi1d	$⊢ x \in On \to (((y \in x \land \emptyset \in y) \land z \in (ω ↑_{𝑜} y)) \leftrightarrow (y \in (x ∖ 1_{𝑜}) \land z \in (ω ↑_{𝑜} y)))$
97	89 96	bitr3id	$⊢ x \in On \to ((y \in x \land (\emptyset \in y \land z \in (ω ↑_{𝑜} y))) \leftrightarrow (y \in (x ∖ 1_{𝑜}) \land z \in (ω ↑_{𝑜} y)))$
98	97	rexbidv2	$⊢ x \in On \to (\exists y \in x (\emptyset \in y \land z \in (ω ↑_{𝑜} y)) \leftrightarrow \exists y \in (x ∖ 1_{𝑜}) z \in (ω ↑_{𝑜} y))$
99	88 98	syl	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (\exists y \in x (\emptyset \in y \land z \in (ω ↑_{𝑜} y)) \leftrightarrow \exists y \in (x ∖ 1_{𝑜}) z \in (ω ↑_{𝑜} y))$
100	87 99	bitr4d	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (z \in (ω ↑_{𝑜} x) \leftrightarrow \exists y \in x (\emptyset \in y \land z \in (ω ↑_{𝑜} y)))$
101		r19.29	$⊢ (\forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land \exists y \in x (\emptyset \in y \land z \in (ω ↑_{𝑜} y))) \to \exists y \in x ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land (\emptyset \in y \land z \in (ω ↑_{𝑜} y)))$
102		id	$⊢ (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)$
103	102	imp	$⊢ ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land \emptyset \in y) \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y$
104	103	anim1i	$⊢ (((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land \emptyset \in y) \land z \in (ω ↑_{𝑜} y)) \to (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))$
105	104	anasss	$⊢ ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land (\emptyset \in y \land z \in (ω ↑_{𝑜} y))) \to (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))$
106	71	ad2antrr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to ω ↑_{𝑜} x \in On$
107		eloni	$⊢ ω ↑_{𝑜} x \in On \to Ord (ω ↑_{𝑜} x)$
108	106 107	syl	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to Ord (ω ↑_{𝑜} x)$
109		simprr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to z \in (ω ↑_{𝑜} y)$
110	64	ad2antrr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to ω \in On$
111	69	ad2antrr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to x \in On$
112		simplr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to y \in x$
113	111 112 90	syl2anc	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to y \in On$
114	110 113 47	syl2anc	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to ω ↑_{𝑜} y \in On$
115		onelon	$⊢ (ω ↑_{𝑜} y \in On \land z \in (ω ↑_{𝑜} y)) \to z \in On$
116	114 109 115	syl2anc	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to z \in On$
117	45	ad2antrr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to A \in On$
118	117	ad2antrr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to A \in On$
119		simplr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to \emptyset \in A$
120	119	ad2antrr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to \emptyset \in A$
121		omord2	$⊢ ((z \in On \land ω ↑_{𝑜} y \in On \land A \in On) \land \emptyset \in A) \to (z \in (ω ↑_{𝑜} y) \leftrightarrow A \cdot_{𝑜} z \in (A \cdot_{𝑜} (ω ↑_{𝑜} y)))$
122	116 114 118 120 121	syl31anc	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to (z \in (ω ↑_{𝑜} y) \leftrightarrow A \cdot_{𝑜} z \in (A \cdot_{𝑜} (ω ↑_{𝑜} y)))$
123	109 122	mpbid	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \in (A \cdot_{𝑜} (ω ↑_{𝑜} y))$
124		simprl	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y$
125	123 124	eleqtrd	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \in (ω ↑_{𝑜} y)$
126	75	ad2antrr	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to ω \in (On ∖ 2_{𝑜})$
127		oeord	$⊢ (y \in On \land x \in On \land ω \in (On ∖ 2_{𝑜})) \to (y \in x \leftrightarrow ω ↑_{𝑜} y \in (ω ↑_{𝑜} x))$
128	113 111 126 127	syl3anc	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to (y \in x \leftrightarrow ω ↑_{𝑜} y \in (ω ↑_{𝑜} x))$
129	112 128	mpbid	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to ω ↑_{𝑜} y \in (ω ↑_{𝑜} x)$
130		ontr1	$⊢ ω ↑_{𝑜} x \in On \to ((A \cdot_{𝑜} z \in (ω ↑_{𝑜} y) \land ω ↑_{𝑜} y \in (ω ↑_{𝑜} x)) \to A \cdot_{𝑜} z \in (ω ↑_{𝑜} x))$
131	106 130	syl	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to ((A \cdot_{𝑜} z \in (ω ↑_{𝑜} y) \land ω ↑_{𝑜} y \in (ω ↑_{𝑜} x)) \to A \cdot_{𝑜} z \in (ω ↑_{𝑜} x))$
132	125 129 131	mp2and	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \in (ω ↑_{𝑜} x)$
133		ordelss	$⊢ (Ord (ω ↑_{𝑜} x) \land A \cdot_{𝑜} z \in (ω ↑_{𝑜} x)) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x$
134	108 132 133	syl2anc	$⊢ ((((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \land (A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x$
135	134	ex	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \to ((A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y \land z \in (ω ↑_{𝑜} y)) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x)$
136	105 135	syl5	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land y \in x) \to (((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land (\emptyset \in y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x)$
137	136	rexlimdva	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to (\exists y \in x ((\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land (\emptyset \in y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x)$
138	101 137	syl5	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to ((\forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \land \exists y \in x (\emptyset \in y \land z \in (ω ↑_{𝑜} y))) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x)$
139	138	expdimp	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (\exists y \in x (\emptyset \in y \land z \in (ω ↑_{𝑜} y)) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x)$
140	100 139	sylbid	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to (z \in (ω ↑_{𝑜} x) \to A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x)$
141	140	ralrimiv	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to \forall z \in (ω ↑_{𝑜} x) A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x$
142		iunss	$⊢ ⋃_{z \in ω ↑_{𝑜} x} (A \cdot_{𝑜} z) \subseteq ω ↑_{𝑜} x \leftrightarrow \forall z \in (ω ↑_{𝑜} x) A \cdot_{𝑜} z \subseteq ω ↑_{𝑜} x$
143	141 142	sylibr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to ⋃_{z \in ω ↑_{𝑜} x} (A \cdot_{𝑜} z) \subseteq ω ↑_{𝑜} x$
144	81 143	eqsstrd	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to A \cdot_{𝑜} (ω ↑_{𝑜} x) \subseteq ω ↑_{𝑜} x$
145		simpllr	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to \emptyset \in A$
146		omword2	$⊢ ((ω ↑_{𝑜} x \in On \land A \in On) \land \emptyset \in A) \to ω ↑_{𝑜} x \subseteq A \cdot_{𝑜} (ω ↑_{𝑜} x)$
147	72 63 145 146	syl21anc	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to ω ↑_{𝑜} x \subseteq A \cdot_{𝑜} (ω ↑_{𝑜} x)$
148	144 147	eqssd	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \land \forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y)) \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x$
149	148	ex	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land Lim x)) \to (\forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x)$
150	149	anassrs	$⊢ (((A \in ω \land \emptyset \in A) \land ω \in On) \land Lim x) \to (\forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x)$
151	150	a1dd	$⊢ (((A \in ω \land \emptyset \in A) \land ω \in On) \land Lim x) \to (\forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in x \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x))$
152	151	expcom	$⊢ Lim x \to (((A \in ω \land \emptyset \in A) \land ω \in On) \to (\forall y \in x (\emptyset \in y \to A \cdot_{𝑜} (ω ↑_{𝑜} y) = ω ↑_{𝑜} y) \to (\emptyset \in x \to A \cdot_{𝑜} (ω ↑_{𝑜} x) = ω ↑_{𝑜} x)))$
153	5 10 15 20 23 62 152	tfinds3	$⊢ B \in On \to (((A \in ω \land \emptyset \in A) \land ω \in On) \to (\emptyset \in B \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B))$
154	153	com12	$⊢ ((A \in ω \land \emptyset \in A) \land ω \in On) \to (B \in On \to (\emptyset \in B \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B))$
155	154	adantrr	$⊢ ((A \in ω \land \emptyset \in A) \land (ω \in On \land B \in On)) \to (B \in On \to (\emptyset \in B \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B))$
156	155	imp32	$⊢ (((A \in ω \land \emptyset \in A) \land (ω \in On \land B \in On)) \land (B \in On \land \emptyset \in B)) \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B$
157	156	an32s	$⊢ (((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \land (ω \in On \land B \in On)) \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B$
158		nnm0	$⊢ A \in ω \to A \cdot_{𝑜} \emptyset = \emptyset$
159	158	ad3antrrr	$⊢ (((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \land \neg (ω \in On \land B \in On)) \to A \cdot_{𝑜} \emptyset = \emptyset$
160		fnoe	$⊢ ↑_{𝑜} Fn (On \times On)$
161		fndm	$⊢ ↑_{𝑜} Fn (On \times On) \to dom ↑_{𝑜} = On \times On$
162	160 161	ax-mp	$⊢ dom ↑_{𝑜} = On \times On$
163	162	ndmov	$⊢ \neg (ω \in On \land B \in On) \to ω ↑_{𝑜} B = \emptyset$
164	163	adantl	$⊢ (((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \land \neg (ω \in On \land B \in On)) \to ω ↑_{𝑜} B = \emptyset$
165	164	oveq2d	$⊢ (((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \land \neg (ω \in On \land B \in On)) \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = A \cdot_{𝑜} \emptyset$
166	159 165 164	3eqtr4d	$⊢ (((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \land \neg (ω \in On \land B \in On)) \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B$
167	157 166	pm2.61dan	$⊢ ((A \in ω \land \emptyset \in A) \land (B \in On \land \emptyset \in B)) \to A \cdot_{𝑜} (ω ↑_{𝑜} B) = ω ↑_{𝑜} B$

Metamath Proof Explorer

Theorem omabs

Proof