Theorem omabs 8614

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 2850	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∅ ∈ 𝑥 ↔ ∅ ∈ ∅))
2		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
3	2	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o ∅)))
4	3, 2	eqeq12d 2777	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
5	1, 4	imbi12d 346	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))))
6		eleq2 2850	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦))
7		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (ω ↑o 𝑥) = (ω ↑o 𝑦))
8	7	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝑦)))
9	8, 7	eqeq12d 2777	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
10	6, 9	imbi12d 346	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))))
11		eleq2 2850	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ suc 𝑦))
12		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (ω ↑o 𝑥) = (ω ↑o suc 𝑦))
13	12	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o suc 𝑦)))
14	13, 12	eqeq12d 2777	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
15	11, 14	imbi12d 346	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
16		eleq2 2850	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵))
17		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (ω ↑o 𝑥) = (ω ↑o 𝐵))
18	17	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝐵)))
19	18, 17	eqeq12d 2777	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))
20	16, 19	imbi12d 346	. . . . . . 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 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ω ∈ On)
25		simpll 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ ω)
26		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ∅ ∈ 𝐴)
27		omabslem 8613	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) = ω)
28	24, 25, 26, 27	syl3anc 1389	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o ω) = ω)
29	28	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o ω) = ω)
30		suceq 6408	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
31		df-1o 8430	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
32	30, 31	eqtr4di 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → suc 𝑦 = 1o)
33	32	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (ω ↑o suc 𝑦) = (ω ↑o 1o))
34		oe1 8506	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
35	34	ad2antrl 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 1o) = ω)
36	33, 35	sylan9eqr 2818	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (ω ↑o suc 𝑦) = ω)
37	36	oveq2d 7406	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ω))
38	29, 37, 36	3eqtr4d 2806	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))
39	38	ex 416	. . . . . . . . . . . 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 7397	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω))
42		oesuc 8489	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
43	42	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
44	43	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
45		nnon 7846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
46	45	ad2antrr 736	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ On)
47		oecl 8499	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o 𝑦) ∈ On)
48	47	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 𝑦) ∈ On)
49		omass 8542	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ ω ∈ On) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
50	46, 48, 24, 49	syl3anc 1389	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
51	44, 50	eqtr4d 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = ((𝐴 ·o (ω ↑o 𝑦)) ·o ω))
52	51, 43	eqeq12d 2777	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦) ↔ ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω)))
53	41, 52	imbitrrid 248	. . . . . . . . . . . . 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 782	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝑦 ∈ On)
57		on0eqel 6465	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
58	56, 57	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
59	40, 55, 58	mpjaod 871	. . . . . . . . . 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 471	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ 𝑦 ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
62	61	expcom 417	. . . . . . 7 ⊢ (𝑦 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))))
63	45	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝐴 ∈ On)
64		simprl 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ On)
65		simprr 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → Lim 𝑥)
66		vex 3457	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
67	65, 66	jctil 527	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (𝑥 ∈ V ∧ Lim 𝑥))
68		limelon 6405	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
69	67, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝑥 ∈ On)
70		oecl 8499	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
71	64, 69, 70	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (ω ↑o 𝑥) ∈ On)
72	71	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
73		1onn 8603	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ ω
74		ondif2 8464	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
75	64, 73, 74	sylanblrc 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ (On ∖ 2o))
76	75	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
77	67	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑥 ∈ V ∧ Lim 𝑥))
78		oelimcl 8563	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ (On ∖ 2o) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (ω ↑o 𝑥))
79	76, 77, 78	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → Lim (ω ↑o 𝑥))
80		omlim 8495	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ ((ω ↑o 𝑥) ∈ On ∧ Lim (ω ↑o 𝑥))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
81	63, 72, 79, 80	syl12anc 847	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
82		simplrl 786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ On)
83		oelim2 8558	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
84	82, 77, 83	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
85	84	eleq2d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ 𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦)))
86		eliun 4952	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))
87	85, 86	bitrdi 289	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
88	69	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝑥 ∈ On)
89		anass 472	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
90		onelon 6365	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
91		on0eln0 6397	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
93	92	pm5.32da 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅)))
94		dif1o 8462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝑥 ∖ 1o) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅))
95	93, 94	bitr4di 291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ 𝑦 ∈ (𝑥 ∖ 1o)))
96	95	anbi1d 640	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
97	89, 96	bitr3id 287	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
98	97	rexbidv2 3181	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
99	88, 98	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
100	87, 99	bitr4d 284	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
101		r19.29 3124	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
102		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
103	102	imp 410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
104	103	anim1i 624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
105	104	anasss 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
106	71	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
107		eloni 6350	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ↑o 𝑥) ∈ On → Ord (ω ↑o 𝑥))
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → Ord (ω ↑o 𝑥))
109		simprr 782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ (ω ↑o 𝑦))
110	64	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ On)
111	69	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑥 ∈ On)
112		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ 𝑥)
113	111, 112, 90	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ On)
114	110, 113, 47	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ On)
115		onelon 6365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ω ↑o 𝑦) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑦)) → 𝑧 ∈ On)
116	114, 109, 115	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ On)
117	45	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝐴 ∈ On)
118	117	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝐴 ∈ On)
119		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ∅ ∈ 𝐴)
120	119	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
121		omord2 8529	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑧 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
122	116, 114, 118, 120, 121	syl31anc 1391	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
123	109, 122	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦)))
124		simprl 780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
125	123, 124	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦))
126	75	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
127		oeord 8551	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
128	113, 111, 126, 127	syl3anc 1389	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
129	112, 128	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ (ω ↑o 𝑥))
130		ontr1 6387	. . . . . . . . . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥))
133		ordelss 6356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (ω ↑o 𝑥) ∧ (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
134	108, 132, 133	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
135	134	ex 416	. . . . . . . . . . . . . . . . . . . 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 3162	. . . . . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
140	100, 139	sylbid 242	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
141	140	ralrimiv 3152	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
142		iunss 5001	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥) ↔ ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
143	141, 142	sylibr 236	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
144	81, 143	eqsstrd 3970	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) ⊆ (ω ↑o 𝑥))
145		simpllr 785	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
146		omword2 8536	. . . . . . . . . . . . 13 ⊢ ((((ω ↑o 𝑥) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
147	72, 63, 145, 146	syl21anc 848	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
148	144, 147	eqssd 3953	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))
149	148	ex 416	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
150	149	anassrs 471	. . . . . . . . 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 417	. . . . . . 7 ⊢ (Lim 𝑥 → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))))
153	5, 10, 15, 20, 23, 62, 152	tfinds3 7839	. . . . . 6 ⊢ (𝐵 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
154	153	com12 32	. . . . 5 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
155	154	adantrr 727	. . . 4 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
156	155	imp32 422	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
157	156	an32s 662	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
158		nnm0 8568	. . . 4 ⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅)
159	158	ad3antrrr 740	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o ∅) = ∅)
160		fnoe 8472	. . . . . . 7 ⊢ ↑o Fn (On × On)
161		fndm 6618	. . . . . . 7 ⊢ ( ↑o Fn (On × On) → dom ↑o = (On × On))
162	160, 161	ax-mp 5	. . . . . 6 ⊢ dom ↑o = (On × On)
163	162	ndmov 7574	. . . . 5 ⊢ (¬ (ω ∈ On ∧ 𝐵 ∈ On) → (ω ↑o 𝐵) = ∅)
164	163	adantl 485	. . . 4 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (ω ↑o 𝐵) = ∅)
165	164	oveq2d 7406	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (𝐴 ·o ∅))
166	159, 165, 164	3eqtr4d 2806	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
167	157, 166	pm2.61dan 822	1 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1559   ∈ wcel 2141   ≠ wne 2956  ∀wral 3075  ∃wrex 3085  Vcvv 3453   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285  ∪ ciun 4948   × cxp 5643  dom cdm 5645  Ord word 6339  Oncon0 6340  Lim wlim 6341  suc csuc 6342   Fn wfn 6510  (class class class)co 7390  ωcom 7840  1_oc1o 8423  2_oc2o 8424   ·_o comu 8428   ↑_o coe 8429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7841  df-1st 7964  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-1o 8430  df-2o 8431  df-oadd 8434  df-omul 8435  df-oexp 8436

This theorem is referenced by:  cnfcom3  9654  omabs2  43862