Theorem omabs 8670

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 2814	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∅ ∈ 𝑥 ↔ ∅ ∈ ∅))
2		oveq2 7425	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
3	2	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o ∅)))
4	3, 2	eqeq12d 2741	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅)))
5	1, 4	imbi12d 343	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ ∅ → (𝐴 ·o (ω ↑o ∅)) = (ω ↑o ∅))))
6		eleq2 2814	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦))
7		oveq2 7425	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (ω ↑o 𝑥) = (ω ↑o 𝑦))
8	7	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝑦)))
9	8, 7	eqeq12d 2741	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
10	6, 9	imbi12d 343	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))))
11		eleq2 2814	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ suc 𝑦))
12		oveq2 7425	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → (ω ↑o 𝑥) = (ω ↑o suc 𝑦))
13	12	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o suc 𝑦)))
14	13, 12	eqeq12d 2741	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)))
15	11, 14	imbi12d 343	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
16		eleq2 2814	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵))
17		oveq2 7425	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (ω ↑o 𝑥) = (ω ↑o 𝐵))
18	17	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑥 = 𝐵 → (𝐴 ·o (ω ↑o 𝑥)) = (𝐴 ·o (ω ↑o 𝐵)))
19	18, 17	eqeq12d 2741	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → ((𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥) ↔ (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))
20	16, 19	imbi12d 343	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)) ↔ (∅ ∈ 𝐵 → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))))
21		noel 4331	. . . . . . . . 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 8669	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) = ω)
28	24, 25, 26, 27	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o ω) = ω)
29	28	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o ω) = ω)
30		suceq 6435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
31		df-1o 8485	. . . . . . . . . . . . . . . . . 18 ⊢ 1o = suc ∅
32	30, 31	eqtr4di 2783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = ∅ → suc 𝑦 = 1o)
33	32	oveq2d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ∅ → (ω ↑o suc 𝑦) = (ω ↑o 1o))
34		oe1 8563	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
35	34	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 1o) = ω)
36	33, 35	sylan9eqr 2787	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (ω ↑o suc 𝑦) = ω)
37	36	oveq2d 7433	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ω))
38	29, 37, 36	3eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) ∧ 𝑦 = ∅) → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))
39	38	ex 411	. . . . . . . . . . . 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 7424	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω))
42		oesuc 8546	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
43	42	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o ω))
44	43	oveq2d 7433	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o (ω ↑o suc 𝑦)) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
45		nnon 7875	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
46	45	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → 𝐴 ∈ On)
47		oecl 8556	. . . . . . . . . . . . . . . . . 18 ⊢ ((ω ∈ On ∧ 𝑦 ∈ On) → (ω ↑o 𝑦) ∈ On)
48	47	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → (ω ↑o 𝑦) ∈ On)
49		omass 8599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ ω ∈ On) → ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω ↑o 𝑦) ·o ω)))
50	46, 48, 24, 49	syl3anc 1368	. . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝑦 ∈ On)) → ((𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦) ↔ ((𝐴 ·o (ω ↑o 𝑦)) ·o ω) = ((ω ↑o 𝑦) ·o ω)))
53	41, 52	imbitrrid 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 6493	. . . . . . . . . . . 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 466	. . . . . . . 8 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) ∧ 𝑦 ∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))))
62	61	expcom 412	. . . . . . 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 3467	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
67	65, 66	jctil 518	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (𝑥 ∈ V ∧ Lim 𝑥))
68		limelon 6433	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
69	67, 68	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → 𝑥 ∈ On)
70		oecl 8556	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
71	64, 69, 70	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (ω ↑o 𝑥) ∈ On)
72	71	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
73		1onn 8659	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ ω
74		ondif2 8521	. . . . . . . . . . . . . . . . 17 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
75	64, 73, 74	sylanblrc 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → ω ∈ (On ∖ 2o))
76	75	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
77	67	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑥 ∈ V ∧ Lim 𝑥))
78		oelimcl 8619	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ (On ∖ 2o) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (ω ↑o 𝑥))
79	76, 77, 78	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → Lim (ω ↑o 𝑥))
80		omlim 8552	. . . . . . . . . . . . . 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 8614	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
84	82, 77, 83	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦))
85	84	eleq2d 2811	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ 𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦)))
86		eliun 5000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω ↑o 𝑦) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))
87	85, 86	bitrdi 286	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦)))
88	69	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → 𝑥 ∈ On)
89		anass 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
90		onelon 6394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
91		on0eln0 6425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅))
93	92	pm5.32da 577	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅)))
94		dif1o 8519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝑥 ∖ 1o) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅))
95	93, 94	bitr4di 288	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ 𝑦 ∈ (𝑥 ∖ 1o)))
96	95	anbi1d 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
97	89, 96	bitr3id 284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω ↑o 𝑦))))
98	97	rexbidv2 3165	. . . . . . . . . . . . . . . . . 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 3104	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))))
102		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)))
103	102	imp 405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))
104	103	anim1i 613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
105	104	anasss 465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)))
106	71	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On)
107		eloni 6379	. . . . . . . . . . . . . . . . . . . . . . 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 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ On)
114	110, 113, 47	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω ↑o 𝑦) ∈ On)
115		onelon 6394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ω ↑o 𝑦) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑦)) → 𝑧 ∈ On)
116	114, 109, 115	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 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 8586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑧 ∈ On ∧ (ω ↑o 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω ↑o 𝑦))))
122	116, 114, 118, 120, 121	syl31anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . 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 2827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦))
126	75	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ (On ∖ 2o))
127		oeord 8607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω ↑o 𝑥)))
128	113, 111, 126, 127	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . 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 6415	. . . . . . . . . . . . . . . . . . . . . . . 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 6385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Ord (ω ↑o 𝑥) ∧ (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
134	108, 132, 133	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
135	134	ex 411	. . . . . . . . . . . . . . . . . . . 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 3145	. . . . . . . . . . . . . . . . . 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 451	. . . . . . . . . . . . . . . 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 3135	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))
142		iunss 5048	. . . . . . . . . . . . . 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 4016	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) ⊆ (ω ↑o 𝑥))
145		simpllr 774	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → ∅ ∈ 𝐴)
146		omword2 8593	. . . . . . . . . . . . 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 3995	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ ∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦))) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥))
149	148	ex 411	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))
150	149	anassrs 466	. . . . . . . . 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 412	. . . . . . 7 ⊢ (Lim 𝑥 → (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ω ∈ On) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω ↑o 𝑥)) = (ω ↑o 𝑥)))))
153	5, 10, 15, 20, 23, 62, 152	tfinds3 7868	. . . . . 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 417	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
157	156	an32s 650	. 2 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
158		nnm0 8624	. . . 4 ⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅)
159	158	ad3antrrr 728	. . 3 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o ∅) = ∅)
160		fnoe 8529	. . . . . . 7 ⊢ ↑o Fn (On × On)
161		fndm 6656	. . . . . . 7 ⊢ ( ↑o Fn (On × On) → dom ↑o = (On × On))
162	160, 161	ax-mp 5	. . . . . 6 ⊢ dom ↑o = (On × On)
163	162	ndmov 7603	. . . . 5 ⊢ (¬ (ω ∈ On ∧ 𝐵 ∈ On) → (ω ↑o 𝐵) = ∅)
164	163	adantl 480	. . . 4 ⊢ ((((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) ∧ ¬ (ω ∈ On ∧ 𝐵 ∈ On)) → (ω ↑o 𝐵) = ∅)
165	164	oveq2d 7433	. . 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 811	1 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098   ≠ wne 2930  ∀wral 3051  ∃wrex 3060  Vcvv 3463   ∖ cdif 3942   ⊆ wss 3945  ∅c0 4323  ∪ ciun 4996   × cxp 5675  dom cdm 5677  Ord word 6368  Oncon0 6369  Lim wlim 6370  suc csuc 6371   Fn wfn 6542  (class class class)co 7417  ωcom 7869  1_oc1o 8478  2_oc2o 8479   ·_o comu 8483   ↑_o coe 8484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-1st 7992  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-oadd 8489  df-omul 8490  df-oexp 8491

This theorem is referenced by:  cnfcom3  9727  omabs2  42826