Theorem omabs 8642

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

Assertion

Ref	Expression
omabs	⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))

Proof of Theorem omabs

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2851	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∅ ∈ 𝑥 ↔ ∅ ∈ ∅))
2		oveq2 7424	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
3	2	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o ∅)))
4	3, 2	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
5	1, 4	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))))
6		eleq2 2851	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦))
7		oveq2 7424	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (ω ↑o 𝑥) = (ω ↑o 𝑦))
8	7	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝑦)))
9	8, 7	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
10	6, 9	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))))
11		eleq2 2851	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ suc 𝑦))
12		oveq2 7424	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (ω ↑o 𝑥) = (ω ↑o suc 𝑦))
13	12	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o suc 𝑦)))
14	13, 12	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
15	11, 14	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
16		eleq2 2851	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵))
17		oveq2 7424	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (ω ↑o 𝑥) = (ω ↑o 𝐵))
18	17	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝐵)))
19	18, 17	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))
20	16, 19	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
21		noel 4287	. . . . . . . . 9 ⊢ ¬ ∅ ∈ ∅
22	21	pm2.21i 120	. . . . . . . 8 ⊢ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))
23	22	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
24		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ω ∈ On)
25		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ ω)
26		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ∅ ∈ 𝐴)
27		omabslem 8641	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) = ω)
28	24, 25, 26, 27	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o ω) = ω)
29	28	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o ω) = ω)
30		suceq 6430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
31		df-1o 8458	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
32	30, 31	eqtr4di 2815	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → suc 𝑦 = 1o)
33	32	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (ω ↑o suc 𝑦) = (ω ↑o 1o))
34		oe1 8534	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
35	34	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 1o) = ω)
36	33, 35	sylan9eqr 2819	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (ω ↑o suc 𝑦) = ω)
37	36	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ω))
38	29, 37, 36	3eqtr4d 2807	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))
39	38	ex 418	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
40	39	a1dd 51	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
41		oveq1 7423	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω))
42		oesuc 8517	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
43	42	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
44	43	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
45		nnon 7871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
46	45	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ On)
47		oecl 8527	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o 𝑦) ∈ On)
48	47	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 𝑦) ∈ On)
49		omass 8570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ ω ∈ On) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
50	46, 48, 24, 49	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
51	44, 50	eqtr4d 2800	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = ((𝐴 ·o (ω ↑o 𝑦)) ·o ω))
52	51, 43	eqeq12d 2778	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦) ↔ ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω)))
53	41, 52	imbitrrid 249	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
54	53	imim2d 58	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
55	54	com23 87	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (∅ ∈ 𝑦 → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
56		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝑦 ∈ On)
57		on0eqel 6487	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
58	56, 57	syl 18	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
59	40, 55, 58	mpjaod 874	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
60	59	a1dd 51	. . . . . . . . 9 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
61	60	anassrs 473	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ 𝑦 ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
62	61	expcom 419	. . . . . . 7 ⊢ (𝑦 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))))
63	45	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝐴 ∈ On)
64		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ On)
65		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → Lim 𝑥)
66		vex 3457	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
67	65, 66	jctil 529	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (𝑥 ∈ V ∧ Lim 𝑥))
68		limelon 6427	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
69	67, 68	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝑥 ∈ On)
70		oecl 8527	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
71	64, 69, 70	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (ω ↑o 𝑥) ∈ On)
72	71	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
73		1onn 8631	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ ω
74		ondif2 8492	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
75	64, 73, 74	sylanblrc 602	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ (On ∖ 2o))
76	75	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
77	67	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑥 ∈ V ∧ Lim 𝑥))
78		oelimcl 8591	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ (On ∖ 2o) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (ω ↑o 𝑥))
79	76, 77, 78	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → Lim (ω ↑o 𝑥))
80		omlim 8523	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ ((ω ↑o 𝑥) ∈ On ∧ Lim (ω ↑o 𝑥))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
81	63, 72, 79, 80	syl12anc 850	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
82		simplrl 789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ On)
83		oelim2 8586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
84	82, 77, 83	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
85	84	eleq2d 2848	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ 𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦)))
86		eliun 4958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))
87	85, 86	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
88	69	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝑥 ∈ On)
89		anass 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
90		onelon 6386	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
91		on0eln0 6419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
92	90, 91	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
93	92	pm5.32da 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅)))
94		dif1o 8490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝑥 ∖ 1o) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅))
95	93, 94	bitr4di 292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ 𝑦 ∈ (𝑥 ∖ 1o)))
96	95	anbi1d 643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
97	89, 96	bitr3id 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
98	97	rexbidv2 3184	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
99	88, 98	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
100	87, 99	bitr4d 285	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
101		r19.29 3127	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
102		id 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
103	102	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
104	103	anim1i 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
105	104	anasss 472	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
106	71	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
107		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ↑o 𝑥) ∈ On → Ord (ω ↑o 𝑥))
108	106, 107	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → Ord (ω ↑o 𝑥))
109		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ (ω ↑o 𝑦))
110	64	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ On)
111	69	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑥 ∈ On)
112		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ 𝑥)
113	111, 112, 90	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ On)
114	110, 113, 47	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ On)
115		onelon 6386	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ω ↑o 𝑦) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑦)) → 𝑧 ∈ On)
116	114, 109, 115	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ On)
117	45	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝐴 ∈ On)
118	117	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝐴 ∈ On)
119		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ∅ ∈ 𝐴)
120	119	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
121		omord2 8557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑧 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
122	116, 114, 118, 120, 121	syl31anc 1400	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
123	109, 122	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦)))
124		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
125	123, 124	eleqtrd 2864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦))
126	75	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
127		oeord 8579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
128	113, 111, 126, 127	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
129	112, 128	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ (ω ↑o 𝑥))
130		ontr1 6409	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ↑o 𝑥) ∈ On → (((𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦) ∧ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)))
131	106, 130	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (((𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦) ∧ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)))
132	125, 129, 131	mp2and 712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥))
133		ordelss 6377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (ω ↑o 𝑥) ∧ (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
134	108, 132, 133	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
135	134	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) → (((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
136	105, 135	syl5 35	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) → (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
137	136	rexlimdva 3165	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
138	101, 137	syl5 35	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
139	138	expdimp 458	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
140	100, 139	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
141	140	ralrimiv 3155	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
142		iunss 5007	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥) ↔ ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
143	141, 142	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
144	81, 143	eqsstrd 3968	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) ⊆ (ω ↑o 𝑥))
145		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
146		omword2 8564	. . . . . . . . . . . . 13 ⊢ ((((ω ↑o 𝑥) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
147	72, 63, 145, 146	syl21anc 851	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
148	144, 147	eqssd 3951	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))
149	148	ex 418	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
150	149	anassrs 473	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
151	150	a1dd 51	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))))
152	151	expcom 419	. . . . . . 7 ⊢ (Lim 𝑥 → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))))
153	5, 10, 15, 20, 23, 62, 152	tfinds3 7864	. . . . . 6 ⊢ (𝐵 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
154	153	com12 33	. . . . 5 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
155	154	adantrr 730	. . . 4 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
156	155	imp32 424	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
157	156	an32s 665	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
158		nnm0 8596	. . . 4 ⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅)
159	158	ad3antrrr 743	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o ∅) = ∅)
160		fnoe 8500	. . . . . . 7 ⊢ ↑o Fn (On × On)
161		fndm 6639	. . . . . . 7 ⊢ ( ↑o Fn (On × On) → dom ↑o = (On × On))
162	160, 161	ax-mp 5	. . . . . 6 ⊢ dom ↑o = (On × On)
163	162	ndmov 7601	. . . . 5 ⊢ (¬ (ω ∈ On ∧ 𝐵 ∈ On) → (ω ↑o 𝐵) = ∅)
164	163	adantl 487	. . . 4 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (ω ↑o 𝐵) = ∅)
165	164	oveq2d 7432	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (𝐴 ·o ∅))
166	159, 165, 164	3eqtr4d 2807	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
167	157, 166	pm2.61dan 825	1 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ∖ cdif 3899   ⊆ wss 3902  ∅c0 4282  ∪ ciun 4954   × cxp 5657  dom cdm 5659  Ord word 6360  Oncon0 6361  Lim wlim 6362  suc csuc 6363   Fn wfn 6532  (class class class)co 7416  ωcom 7865  1_oc1o 8451  2_oc2o 8452   ·_o comu 8456   ↑_o coe 8457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-oadd 8462  df-omul 8463  df-oexp 8464

This theorem is used by:  cnfcom3  9686  omabs2  44160