Theorem omabs 8597

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 2826	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∅ ∈ 𝑥 ↔ ∅ ∈ ∅))
2		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
3	2	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o ∅)))
4	3, 2	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
5	1, 4	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))))
6		eleq2 2826	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦))
7		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (ω ↑o 𝑥) = (ω ↑o 𝑦))
8	7	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝑦)))
9	8, 7	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
10	6, 9	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))))
11		eleq2 2826	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ suc 𝑦))
12		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (ω ↑o 𝑥) = (ω ↑o suc 𝑦))
13	12	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o suc 𝑦)))
14	13, 12	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
15	11, 14	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
16		eleq2 2826	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵))
17		oveq2 7365	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (ω ↑o 𝑥) = (ω ↑o 𝐵))
18	17	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝐵)))
19	18, 17	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))
20	16, 19	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
21		noel 4290	. . . . . . . . 9 ⊢ ¬ ∅ ∈ ∅
22	21	pm2.21i 119	. . . . . . . 8 ⊢ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))
23	22	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
24		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ω ∈ On)
25		simpll 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ ω)
26		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ∅ ∈ 𝐴)
27		omabslem 8596	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) = ω)
28	24, 25, 26, 27	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o ω) = ω)
29	28	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o ω) = ω)
30		suceq 6383	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
31		df-1o 8412	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
32	30, 31	eqtr4di 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → suc 𝑦 = 1o)
33	32	oveq2d 7373	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (ω ↑o suc 𝑦) = (ω ↑o 1o))
34		oe1 8491	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
35	34	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 1o) = ω)
36	33, 35	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (ω ↑o suc 𝑦) = ω)
37	36	oveq2d 7373	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ω))
38	29, 37, 36	3eqtr4d 2786	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))
39	38	ex 413	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
40	39	a1dd 50	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
41		oveq1 7364	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω))
42		oesuc 8473	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
43	42	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
44	43	oveq2d 7373	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
45		nnon 7808	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
46	45	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ On)
47		oecl 8483	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o 𝑦) ∈ On)
48	47	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 𝑦) ∈ On)
49		omass 8527	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ ω ∈ On) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
50	46, 48, 24, 49	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
51	44, 50	eqtr4d 2779	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = ((𝐴 ·o (ω ↑o 𝑦)) ·o ω))
52	51, 43	eqeq12d 2752	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦) ↔ ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω)))
53	41, 52	syl5ibr 245	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
54	53	imim2d 57	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
55	54	com23 86	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (∅ ∈ 𝑦 → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
56		simprr 771	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝑦 ∈ On)
57		on0eqel 6441	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
58	56, 57	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
59	40, 55, 58	mpjaod 858	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
60	59	a1dd 50	. . . . . . . . 9 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
61	60	anassrs 468	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ 𝑦 ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
62	61	expcom 414	. . . . . . 7 ⊢ (𝑦 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))))
63	45	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝐴 ∈ On)
64		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ On)
65		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → Lim 𝑥)
66		vex 3449	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
67	65, 66	jctil 520	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (𝑥 ∈ V ∧ Lim 𝑥))
68		limelon 6381	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
69	67, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝑥 ∈ On)
70		oecl 8483	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
71	64, 69, 70	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (ω ↑o 𝑥) ∈ On)
72	71	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
73		1onn 8586	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ ω
74		ondif2 8448	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
75	64, 73, 74	sylanblrc 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ (On ∖ 2o))
76	75	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
77	67	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑥 ∈ V ∧ Lim 𝑥))
78		oelimcl 8547	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ (On ∖ 2o) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (ω ↑o 𝑥))
79	76, 77, 78	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → Lim (ω ↑o 𝑥))
80		omlim 8479	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ ((ω ↑o 𝑥) ∈ On ∧ Lim (ω ↑o 𝑥))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
81	63, 72, 79, 80	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
82		simplrl 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ On)
83		oelim2 8542	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
84	82, 77, 83	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
85	84	eleq2d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ 𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦)))
86		eliun 4958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))
87	85, 86	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
88	69	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝑥 ∈ On)
89		anass 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
90		onelon 6342	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
91		on0eln0 6373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
93	92	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅)))
94		dif1o 8446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝑥 ∖ 1o) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅))
95	93, 94	bitr4di 288	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ 𝑦 ∈ (𝑥 ∖ 1o)))
96	95	anbi1d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
97	89, 96	bitr3id 284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
98	97	rexbidv2 3171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
99	88, 98	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
100	87, 99	bitr4d 281	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
101		r19.29 3117	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
102		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
103	102	imp 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
104	103	anim1i 615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
105	104	anasss 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
106	71	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
107		eloni 6327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ↑o 𝑥) ∈ On → Ord (ω ↑o 𝑥))
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → Ord (ω ↑o 𝑥))
109		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ (ω ↑o 𝑦))
110	64	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ On)
111	69	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑥 ∈ On)
112		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ 𝑥)
113	111, 112, 90	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ On)
114	110, 113, 47	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ On)
115		onelon 6342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ω ↑o 𝑦) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑦)) → 𝑧 ∈ On)
116	114, 109, 115	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ On)
117	45	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝐴 ∈ On)
118	117	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝐴 ∈ On)
119		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ∅ ∈ 𝐴)
120	119	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
121		omord2 8514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑧 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
122	116, 114, 118, 120, 121	syl31anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
123	109, 122	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦)))
124		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
125	123, 124	eleqtrd 2840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦))
126	75	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
127		oeord 8535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
128	113, 111, 126, 127	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
129	112, 128	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ (ω ↑o 𝑥))
130		ontr1 6363	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ↑o 𝑥) ∈ On → (((𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦) ∧ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)))
131	106, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (((𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦) ∧ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)))
132	125, 129, 131	mp2and 697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥))
133		ordelss 6333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (ω ↑o 𝑥) ∧ (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
134	108, 132, 133	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
135	134	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) → (((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
136	105, 135	syl5 34	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) → (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
137	136	rexlimdva 3152	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
138	101, 137	syl5 34	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
139	138	expdimp 453	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
140	100, 139	sylbid 239	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
141	140	ralrimiv 3142	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
142		iunss 5005	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥) ↔ ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
143	141, 142	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
144	81, 143	eqsstrd 3982	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) ⊆ (ω ↑o 𝑥))
145		simpllr 774	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
146		omword2 8521	. . . . . . . . . . . . 13 ⊢ ((((ω ↑o 𝑥) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
147	72, 63, 145, 146	syl21anc 836	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
148	144, 147	eqssd 3961	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))
149	148	ex 413	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
150	149	anassrs 468	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
151	150	a1dd 50	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))))
152	151	expcom 414	. . . . . . 7 ⊢ (Lim 𝑥 → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))))
153	5, 10, 15, 20, 23, 62, 152	tfinds3 7801	. . . . . 6 ⊢ (𝐵 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
154	153	com12 32	. . . . 5 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
155	154	adantrr 715	. . . 4 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
156	155	imp32 419	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
157	156	an32s 650	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
158		nnm0 8552	. . . 4 ⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅)
159	158	ad3antrrr 728	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o ∅) = ∅)
160		fnoe 8456	. . . . . . 7 ⊢ ↑o Fn (On × On)
161		fndm 6605	. . . . . . 7 ⊢ ( ↑o Fn (On × On) → dom ↑o = (On × On))
162	160, 161	ax-mp 5	. . . . . 6 ⊢ dom ↑o = (On × On)
163	162	ndmov 7538	. . . . 5 ⊢ (¬ (ω ∈ On ∧ 𝐵 ∈ On) → (ω ↑o 𝐵) = ∅)
164	163	adantl 482	. . . 4 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (ω ↑o 𝐵) = ∅)
165	164	oveq2d 7373	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (𝐴 ·o ∅))
166	159, 165, 164	3eqtr4d 2786	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
167	157, 166	pm2.61dan 811	1 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  Vcvv 3445   ∖ cdif 3907   ⊆ wss 3910  ∅c0 4282  ∪ ciun 4954   × cxp 5631  dom cdm 5633  Ord word 6316  Oncon0 6317  Lim wlim 6318  suc csuc 6319   Fn wfn 6491  (class class class)co 7357  ωcom 7802  1_oc1o 8405  2_oc2o 8406   ·_o comu 8410   ↑_o coe 8411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-oexp 8418

This theorem is referenced by:  cnfcom3  9640  omabs2  41651