Theorem omabs 8618

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 2818	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∅ ∈ 𝑥 ↔ ∅ ∈ ∅))
2		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
3	2	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o ∅)))
4	3, 2	eqeq12d 2746	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
5	1, 4	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))))
6		eleq2 2818	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦))
7		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (ω ↑o 𝑥) = (ω ↑o 𝑦))
8	7	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝑦)))
9	8, 7	eqeq12d 2746	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
10	6, 9	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))))
11		eleq2 2818	. . . . . . . 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 2746	. . . . . . . 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 2818	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵))
17		oveq2 7398	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (ω ↑o 𝑥) = (ω ↑o 𝐵))
18	17	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝐵)))
19	18, 17	eqeq12d 2746	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))
20	16, 19	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
21		noel 4304	. . . . . . . . 9 ⊢ ¬ ∅ ∈ ∅
22	21	pm2.21i 119	. . . . . . . 8 ⊢ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))
23	22	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
24		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ω ∈ On)
25		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ ω)
26		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ∅ ∈ 𝐴)
27		omabslem 8617	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) = ω)
28	24, 25, 26, 27	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o ω) = ω)
29	28	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o ω) = ω)
30		suceq 6403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
31		df-1o 8437	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
32	30, 31	eqtr4di 2783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → suc 𝑦 = 1o)
33	32	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (ω ↑o suc 𝑦) = (ω ↑o 1o))
34		oe1 8511	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
35	34	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 1o) = ω)
36	33, 35	sylan9eqr 2787	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (ω ↑o suc 𝑦) = ω)
37	36	oveq2d 7406	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ω))
38	29, 37, 36	3eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))
39	38	ex 412	. . . . . . . . . . . 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 8494	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
43	42	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
44	43	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
45		nnon 7851	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
46	45	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ On)
47		oecl 8504	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o 𝑦) ∈ On)
48	47	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 𝑦) ∈ On)
49		omass 8547	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ ω ∈ On) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
50	46, 48, 24, 49	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
51	44, 50	eqtr4d 2768	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = ((𝐴 ·o (ω ↑o 𝑦)) ·o ω))
52	51, 43	eqeq12d 2746	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦) ↔ ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω)))
53	41, 52	imbitrrid 246	. . . . . . . . . . . . 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 772	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝑦 ∈ On)
57		on0eqel 6461	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ On → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
58	56, 57	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝑦 = ∅ ∨ ∅ ∈ 𝑦))
59	40, 55, 58	mpjaod 860	. . . . . . . . . 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 467	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ 𝑦 ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
62	61	expcom 413	. . . . . . 7 ⊢ (𝑦 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))))
63	45	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝐴 ∈ On)
64		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ On)
65		simprr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → Lim 𝑥)
66		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
67	65, 66	jctil 519	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (𝑥 ∈ V ∧ Lim 𝑥))
68		limelon 6400	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
69	67, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝑥 ∈ On)
70		oecl 8504	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
71	64, 69, 70	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (ω ↑o 𝑥) ∈ On)
72	71	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
73		1onn 8607	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ ω
74		ondif2 8469	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
75	64, 73, 74	sylanblrc 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ (On ∖ 2o))
76	75	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
77	67	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑥 ∈ V ∧ Lim 𝑥))
78		oelimcl 8567	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ (On ∖ 2o) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (ω ↑o 𝑥))
79	76, 77, 78	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → Lim (ω ↑o 𝑥))
80		omlim 8500	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ ((ω ↑o 𝑥) ∈ On ∧ Lim (ω ↑o 𝑥))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
81	63, 72, 79, 80	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧))
82		simplrl 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ On)
83		oelim2 8562	. . . . . . . . . . . . . . . . . . . 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 2815	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ 𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦)))
86		eliun 4962	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))
87	85, 86	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
88	69	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝑥 ∈ On)
89		anass 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
90		onelon 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
91		on0eln0 6392	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
93	92	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅)))
94		dif1o 8467	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝑥 ∖ 1o) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅))
95	93, 94	bitr4di 289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ 𝑦 ∈ (𝑥 ∖ 1o)))
96	95	anbi1d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
97	89, 96	bitr3id 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
98	97	rexbidv2 3154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
99	88, 98	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
100	87, 99	bitr4d 282	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
101		r19.29 3095	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
102		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
103	102	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
104	103	anim1i 615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
105	104	anasss 466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
106	71	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
107		eloni 6345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ↑o 𝑥) ∈ On → Ord (ω ↑o 𝑥))
108	106, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → Ord (ω ↑o 𝑥))
109		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ (ω ↑o 𝑦))
110	64	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ On)
111	69	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑥 ∈ On)
112		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ω ↑o 𝑦) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑦)) → 𝑧 ∈ On)
116	114, 109, 115	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ On)
117	45	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝐴 ∈ On)
118	117	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝐴 ∈ On)
119		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ∅ ∈ 𝐴)
120	119	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
121		omord2 8534	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑧 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
122	116, 114, 118, 120, 121	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
123	109, 122	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦)))
124		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
125	123, 124	eleqtrd 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦))
126	75	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
127		oeord 8555	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
128	113, 111, 126, 127	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
129	112, 128	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ (ω ↑o 𝑥))
130		ontr1 6382	. . . . . . . . . . . . . . . . . . . . . . . 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 699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥))
133		ordelss 6351	. . . . . . . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . . . . . . . . . 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 3135	. . . . . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
140	100, 139	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)))
141	140	ralrimiv 3125	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
142		iunss 5012	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥) ↔ ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
143	141, 142	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
144	81, 143	eqsstrd 3984	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) ⊆ (ω ↑o 𝑥))
145		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
146		omword2 8541	. . . . . . . . . . . . 13 ⊢ ((((ω ↑o 𝑥) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
147	72, 63, 145, 146	syl21anc 837	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω ↑o 𝑥)))
148	144, 147	eqssd 3967	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))
149	148	ex 412	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
150	149	anassrs 467	. . . . . . . . 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 413	. . . . . . 7 ⊢ (Lim 𝑥 → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))))
153	5, 10, 15, 20, 23, 62, 152	tfinds3 7844	. . . . . 6 ⊢ (𝐵 ∈ On → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
154	153	com12 32	. . . . 5 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
155	154	adantrr 717	. . . 4 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐵 ∈ On → (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
156	155	imp32 418	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
157	156	an32s 652	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
158		nnm0 8572	. . . 4 ⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅)
159	158	ad3antrrr 730	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o ∅) = ∅)
160		fnoe 8477	. . . . . . 7 ⊢ ↑o Fn (On × On)
161		fndm 6624	. . . . . . 7 ⊢ ( ↑o Fn (On × On) → dom ↑o = (On × On))
162	160, 161	ax-mp 5	. . . . . 6 ⊢ dom ↑o = (On × On)
163	162	ndmov 7576	. . . . 5 ⊢ (¬ (ω ∈ On ∧ 𝐵 ∈ On) → (ω ↑o 𝐵) = ∅)
164	163	adantl 481	. . . 4 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (ω ↑o 𝐵) = ∅)
165	164	oveq2d 7406	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (𝐴 ·o ∅))
166	159, 165, 164	3eqtr4d 2775	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
167	157, 166	pm2.61dan 812	1 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  Vcvv 3450   ∖ cdif 3914   ⊆ wss 3917  ∅c0 4299  ∪ ciun 4958   × cxp 5639  dom cdm 5641  Ord word 6334  Oncon0 6335  Lim wlim 6336  suc csuc 6337   Fn wfn 6509  (class class class)co 7390  ωcom 7845  1_oc1o 8430  2_oc2o 8431   ·_o comu 8435   ↑_o coe 8436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-oadd 8441  df-omul 8442  df-oexp 8443

This theorem is referenced by:  cnfcom3  9664  omabs2  43328