Theorem omabs2 42764

Description: Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or ω raised to some power of ω. (Contributed by RP, 12-Jan-2025.)

Assertion

Ref	Expression
omabs2	⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)

Proof of Theorem omabs2

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

Step	Hyp	Ref	Expression
1		eleq2 2817	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅))
2		noel 4332	. . . . . . 7 ⊢ ¬ 𝐴 ∈ ∅
3	2	pm2.21i 119	. . . . . 6 ⊢ (𝐴 ∈ ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
4	1, 3	biimtrdi 252	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵)))
5	4	impd 409	. . . 4 ⊢ (𝐵 = ∅ → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
6	5	com12 32	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = 𝐵))
7		elpri 4653	. . . . . . . . 9 ⊢ (𝐴 ∈ {∅, 1o} → (𝐴 = ∅ ∨ 𝐴 = 1o))
8		eleq2 2817	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 ↔ ∅ ∈ ∅))
9		noel 4332	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ ∅
10	9	pm2.21i 119	. . . . . . . . . . 11 ⊢ (∅ ∈ ∅ → (𝐴 ·o 2o) = 2o)
11	8, 10	biimtrdi 252	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
12		oveq1 7431	. . . . . . . . . . . 12 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = (1o ·o 2o))
13		2on 8505	. . . . . . . . . . . . 13 ⊢ 2o ∈ On
14		om1r 8568	. . . . . . . . . . . . 13 ⊢ (2o ∈ On → (1o ·o 2o) = 2o)
15	13, 14	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1o ·o 2o) = 2o
16	12, 15	eqtrdi 2783	. . . . . . . . . . 11 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = 2o)
17	16	a1d 25	. . . . . . . . . 10 ⊢ (𝐴 = 1o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
18	11, 17	jaoi 855	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐴 = 1o) → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
19	7, 18	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ {∅, 1o} → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
20		df2o3 8499	. . . . . . . 8 ⊢ 2o = {∅, 1o}
21	19, 20	eleq2s 2846	. . . . . . 7 ⊢ (𝐴 ∈ 2o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
22	21	imp 405	. . . . . 6 ⊢ ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o)
23	22	a1i 11	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o))
24		eleq2 2817	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o))
25	24	anbi1d 629	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ∈ 2o ∧ ∅ ∈ 𝐴)))
26		oveq2 7432	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ·o 𝐵) = (𝐴 ·o 2o))
27		id 22	. . . . . 6 ⊢ (𝐵 = 2o → 𝐵 = 2o)
28	26, 27	eqeq12d 2743	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o 2o) = 2o))
29	23, 25, 28	3imtr4d 293	. . . 4 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
30	29	com12 32	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = 2o → (𝐴 ·o 𝐵) = 𝐵))
31		simpr 483	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → 𝐴 ∈ ω)
32		simpllr 774	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ 𝐴)
33		omelon 9675	. . . . . . . . . 10 ⊢ ω ∈ On
34		oecl 8562	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
35	33, 34	mpan 688	. . . . . . . . 9 ⊢ (𝐶 ∈ On → (ω ↑o 𝐶) ∈ On)
36	35	adantl 480	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
37	36	ad2antlr 725	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (ω ↑o 𝐶) ∈ On)
38	33	jctl 522	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 𝐶 ∈ On))
39		peano1 7898	. . . . . . . . . 10 ⊢ ∅ ∈ ω
40		oen0 8611	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
41	38, 39, 40	sylancl 584	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ∅ ∈ (ω ↑o 𝐶))
42	41	adantl 480	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ∅ ∈ (ω ↑o 𝐶))
43	42	ad2antlr 725	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
44		omabs 8676	. . . . . . 7 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ((ω ↑o 𝐶) ∈ On ∧ ∅ ∈ (ω ↑o 𝐶))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
45	31, 32, 37, 43, 44	syl22anc 837	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
46		oveq2 7432	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → (𝐴 ·o 𝐵) = (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
47		id 22	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
48	46, 47	eqeq12d 2743	. . . . . . . 8 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
49	48	adantr 479	. . . . . . 7 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
50	49	ad2antlr 725	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
51	45, 50	mpbird 256	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (𝐴 ·o 𝐵) = 𝐵)
52		simpl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
53		oecl 8562	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
54	33, 35, 53	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → (ω ↑o (ω ↑o 𝐶)) ∈ On)
55	54	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
56	52, 55	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
57		simpl 481	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → 𝐴 ∈ 𝐵)
58		onelon 6397	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On)
59	56, 57, 58	syl2anr 595	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ On)
60		simplr 767	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ∅ ∈ 𝐴)
61		ondif1 8526	. . . . . . . . . 10 ⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
62	59, 60, 61	sylanbrc 581	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ (On ∖ 1o))
63		1onn 8665	. . . . . . . . . 10 ⊢ 1o ∈ ω
64		ondif2 8527	. . . . . . . . . 10 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
65	33, 63, 64	mpbir2an 709	. . . . . . . . 9 ⊢ ω ∈ (On ∖ 2o)
66	62, 65	jctil 518	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
67	66	adantr 479	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
68		oeeu 8628	. . . . . . 7 ⊢ ((ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)) → ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
69	67, 68	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
70		euex 2566	. . . . . . 7 ⊢ (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
71		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
72		0ss 4398	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝑧
73		0elon 6426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
74		simpr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
75		oecl 8562	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
76	33, 74, 75	sylancr 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
77	76	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → (ω ↑o 𝑥) ∈ On)
78		onelon 6397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
79	77, 78	sylancom 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
80		1on 8503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1o ∈ On
81		omcl 8561	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 1o ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
82	76, 80, 81	sylancl 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
83	82	ad5ant12 754	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
84		oaword 8574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∅ ∈ On ∧ 𝑧 ∈ On ∧ ((ω ↑o 𝑥) ·o 1o) ∈ On) → (∅ ⊆ 𝑧 ↔ (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
85	84	biimpd 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∅ ∈ On ∧ 𝑧 ∈ On ∧ ((ω ↑o 𝑥) ·o 1o) ∈ On) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
86	73, 79, 83, 85	mp3an2ani 1464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
87	72, 86	mpi 20	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧))
88		simpllr 774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ (ω ∖ 1o))
89		omsson 7878	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ω ⊆ On
90		ssdif 4138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ On → (ω ∖ 1o) ⊆ (On ∖ 1o))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ω ∖ 1o) ⊆ (On ∖ 1o)
92	91	sseli 3976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ (On ∖ 1o))
93		ondif1 8526	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (On ∖ 1o) ↔ (𝑦 ∈ On ∧ ∅ ∈ 𝑦))
94		df-1o 8491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o = suc ∅
95		eloni 6382	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → Ord 𝑦)
96		ordsucss 7825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑦 → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
97	95, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
98	97	imp 405	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → suc ∅ ⊆ 𝑦)
99	94, 98	eqsstrid 4028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → 1o ⊆ 𝑦)
100	93, 99	sylbi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (On ∖ 1o) → 1o ⊆ 𝑦)
101	88, 92, 100	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑦)
102		eldifi 4125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ ω)
103		nnon 7880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ On)
105	104	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑦 ∈ On)
106		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ On)
107	33, 106, 75	sylancr 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ On)
108		omwordi 8596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1o ∈ On ∧ 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
109	80, 105, 107, 108	mp3an2ani 1464	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
110	101, 109	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦))
111	105	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ On)
112		omcl 8561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
113	107, 111, 112	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
114	79	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ On)
115		oawordri 8575	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((ω ↑o 𝑥) ·o 1o) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On ∧ 𝑧 ∈ On) → (((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (((ω ↑o 𝑥) ·o 1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧)))
116	83, 113, 114, 115	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (((ω ↑o 𝑥) ·o 1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧)))
117	110, 116	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
118	87, 117	sstrd 3990	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
119	33, 75	mpan 688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (ω ↑o 𝑥) ∈ On)
120	119, 80, 81	sylancl 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) ∈ On)
121		oa0 8541	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ω ↑o 𝑥) ·o 1o) ∈ On → (((ω ↑o 𝑥) ·o 1o) +o ∅) = ((ω ↑o 𝑥) ·o 1o))
122	120, 121	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → (((ω ↑o 𝑥) ·o 1o) +o ∅) = ((ω ↑o 𝑥) ·o 1o))
123		om1 8567	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ↑o 𝑥) ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
124	119, 123	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
125	122, 124	eqtrd 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ On → (((ω ↑o 𝑥) ·o 1o) +o ∅) = (ω ↑o 𝑥))
126	106, 125	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) = (ω ↑o 𝑥))
127		simpr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
128	118, 126, 127	3sstr3d 4026	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ⊆ 𝐴)
129		simp-7l 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ 𝐵)
130		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
131	130	ad4antr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
132	129, 131	eleqtrd 2830	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
133	55	ad6antlr 735	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
134		ontr2 6419	. . . . . . . . . . . . . . . . 17 ⊢ (((ω ↑o 𝑥) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
135	107, 133, 134	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
136	128, 132, 135	mp2and 697	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶)))
137	36	ad6antlr 735	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝐶) ∈ On)
138	65	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ∈ (On ∖ 2o))
139		oeord 8613	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
140	106, 137, 138, 139	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
141	136, 140	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ (ω ↑o 𝐶))
142		simp-5r 784	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ 𝐴)
143	142, 128	unssd 4186	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
144		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ (ω ↑o 𝑥))
145		onelpss 6412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) ↔ (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
146	145	biimpd 228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
147	79, 107, 146	syl2an2r 683	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
148	144, 147	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)))
149		simpl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)) → 𝑧 ⊆ (ω ↑o 𝑥))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ⊆ (ω ↑o 𝑥))
151		oaword 8574	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) ↔ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
152	151	biimpd 228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
153	114, 107, 113, 152	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
154	150, 153	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
155		omsuc 8551	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
156	107, 111, 155	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
157	154, 156	sseqtrrd 4021	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o suc 𝑦))
158		ordom 7884	. . . . . . . . . . . . . . . . . . 19 ⊢ Ord ω
159	88, 102	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ ω)
160		ordsucss 7825	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ω → (𝑦 ∈ ω → suc 𝑦 ⊆ ω))
161	158, 159, 160	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ ω)
162		oe1 8569	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
163	33, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ↑o 1o) = ω
164		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑥 = ∅)
165	164	oveq2d 7440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = (ω ↑o ∅))
166		oe0 8547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ∈ On → (ω ↑o ∅) = 1o)
167	33, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) = 1o
168	165, 167	eqtrdi 2783	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = 1o)
169	168	oveq1d 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = (1o ·o 𝑦))
170	104	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → 𝑦 ∈ On)
171	170	ad5ant12 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ On)
172		om1r 8568	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → (1o ·o 𝑦) = 𝑦)
173	171, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (1o ·o 𝑦) = 𝑦)
174	169, 173	eqtrd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = 𝑦)
175		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ (ω ↑o 𝑥))
176	175, 168	eleqtrd 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ 1o)
177		el1o 8520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 1o ↔ 𝑧 = ∅)
178	176, 177	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 = ∅)
179	174, 178	oveq12d 7442	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = (𝑦 +o ∅))
180		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
181		oa0 8541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ On → (𝑦 +o ∅) = 𝑦)
182	171, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (𝑦 +o ∅) = 𝑦)
183	179, 180, 182	3eqtr3d 2775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 = 𝑦)
184	159	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ ω)
185	183, 184	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 ∈ ω)
186	185	ex 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 𝐴 ∈ ω))
187	33, 33	pm3.2i 469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ On ∧ ω ∈ On)
188		ontr2 6419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ ω ∈ On) → ((ω ⊆ 𝐴 ∧ 𝐴 ∈ ω) → ω ∈ ω))
189	188	expd 414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ ω ∈ On) → (ω ⊆ 𝐴 → (𝐴 ∈ ω → ω ∈ ω)))
190	187, 142, 189	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ∈ ω → ω ∈ ω))
191		elirr 9626	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ω ∈ ω
192	191	pm2.21i 119	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ ω → 1o ⊆ 𝑥)
193	192	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∈ ω → 1o ⊆ 𝑥))
194	186, 190, 193	3syld 60	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 1o ⊆ 𝑥))
195		eloni 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → Ord 𝑥)
196		ordsucss 7825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
197	196	imp 405	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
198	94, 197	eqsstrid 4028	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
199	198	ex 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
200	106, 195, 199	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
201		on0eqel 6496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
202	106, 201	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
203	194, 200, 202	mpjaod 858	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑥)
204	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ∈ On)
205	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ∈ On)
206	204, 106, 205	3jca 1125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On))
207		oewordi 8616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
208	206, 39, 207	sylancl 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
209	203, 208	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
210	163, 209	eqsstrrid 4029	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ (ω ↑o 𝑥))
211	161, 210	sstrd 3990	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ (ω ↑o 𝑥))
212		onsuc 7818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
213	111, 212	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ∈ On)
214		omwordi 8596	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
215	213, 107, 107, 214	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
216	211, 215	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
217	157, 216	sstrd 3990	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
218	127	eqcomd 2733	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 = (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
219		oeoa 8622	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
220	33, 106, 106, 219	mp3an2i 1462	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
221	217, 218, 220	3sstr4d 4027	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
222		simpr3 1193	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
223	59	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ On)
224		simprr 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐶 ∈ On)
225		simp1 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → 𝑥 ∈ (ω ↑o 𝐶))
226	224, 225	anim12i 611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)))
227		onelon 6397	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
228	35, 227	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
229		pm4.24 562	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝑥 ∈ On))
230	228, 229	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 ∈ On ∧ 𝑥 ∈ On))
231		oacl 8560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On) → (𝑥 +o 𝑥) ∈ On)
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 +o 𝑥) ∈ On)
233		oecl 8562	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
234	33, 232, 233	sylancr 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
235	226, 234	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
236	55	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
237		omwordri 8597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ (ω ↑o (𝑥 +o 𝑥)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
238	223, 235, 236, 237	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
239	222, 238	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
240	226, 230, 231	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o 𝑥) ∈ On)
241	36	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ∈ On)
242		oeoa 8622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
243	33, 240, 241, 242	mp3an2i 1462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
244	226, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ On)
245		oaass 8586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
246	244, 244, 241, 245	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
247		simpr1 1191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ (ω ↑o 𝐶))
248		ssidd 4003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
249		oaabs2 8674	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ↑o 𝐶) ∈ On) ∧ (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶)) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
250	247, 241, 248, 249	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
251	250	oveq2d 7440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (𝑥 +o (ω ↑o 𝐶))) = (𝑥 +o (ω ↑o 𝐶)))
252	246, 251, 250	3eqtrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
253	252	oveq2d 7440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
254	243, 253	eqtr3d 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
255	239, 254	sseqtrd 4020	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (ω ↑o (ω ↑o 𝐶)))
256		oveq2 7432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
257	256, 167	eqtrdi 2783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = 1o)
258	257	uneq2d 4162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ∪ 1o))
259	33	oneluni 6491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ∈ ω → (ω ∪ 1o) = ω)
260	63, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ω ∪ 1o) = ω
261	260, 163	eqtr4i 2758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ω ∪ 1o) = (ω ↑o 1o)
262	258, 261	eqtrdi 2783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
263	262	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
264	263	oveq1d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
265	224	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → 𝐶 ∈ On)
266		oecl 8562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((ω ∈ On ∧ ∅ ∈ On) → (ω ↑o ∅) ∈ On)
267	33, 73, 266	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) ∈ On
268		oecl 8562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ∈ On ∧ (ω ↑o ∅) ∈ On) → (ω ↑o (ω ↑o ∅)) ∈ On)
269	33, 267, 268	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ω ↑o (ω ↑o ∅)) ∈ On
270	269	2a1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ On))
271	270, 54	jca2 512	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On)))
272	167	oveq2i 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ω ↑o (ω ↑o ∅)) = (ω ↑o 1o)
273	272, 163	eqtri 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ω ↑o (ω ↑o ∅)) = ω
274		ssun1 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ω ⊆ (ω ∪ (ω ↑o 𝑥))
275	273, 274	eqsstri 4014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ↑o (ω ↑o ∅)) ⊆ (ω ∪ (ω ↑o 𝑥))
276		simp2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
277	275, 276	sstrid 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
278	277	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
279	57	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ 𝐵)
280		simplrl 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
281	279, 280	eleqtrd 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
282	278, 281	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
283	282	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
284		ontr2 6419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
285	271, 283, 284	syl6ci 71	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
286		oeord 8613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
287	73, 65, 286	mp3an13 1448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
288	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐶 ∈ On → ω ∈ (On ∖ 2o))
289		oeord 8613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ω ↑o ∅) ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
290	267, 35, 288, 289	mp3an2i 1462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
291	287, 290	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
292	291	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶)) → ∅ ∈ 𝐶))
293	285, 292	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ∅ ∈ 𝐶))
294		eloni 6382	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → Ord 𝐶)
295		ordsucss 7825	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶))
296	94	sseq1i 4008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶)
297	295, 296	imbitrrdi 251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
298	294, 297	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
299	293, 298	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → 1o ⊆ 𝐶))
300	265, 299	jcai 515	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On ∧ 1o ⊆ 𝐶))
301	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → ω ∈ On)
302	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → 1o ∈ On)
303	301, 302, 35	3jca 1125	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
304	303	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
305		oeoa 8622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
306	304, 305	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
307	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → 1o ∈ ω)
308	35	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 𝐶) ∈ On)
309		oeword 8615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
310	80, 65, 309	mp3an13 1448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
311	310	biimpa 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 1o) ⊆ (ω ↑o 𝐶))
312	163, 311	eqsstrrid 4029	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ω ⊆ (ω ↑o 𝐶))
313		oaabs 8673	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1o ∈ ω ∧ (ω ↑o 𝐶) ∈ On) ∧ ω ⊆ (ω ↑o 𝐶)) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
314	307, 308, 312, 313	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
315	314	oveq2d 7440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
316	306, 315	eqtr3d 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
317	300, 316	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
318	264, 317	eqtrd 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
319	244, 195, 196	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
320	319	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
321	94, 320	eqsstrid 4028	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
322	247	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ (ω ↑o 𝐶))
323	241, 322, 227	syl2an2r 683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ On)
324	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ∈ (On ∖ 2o))
325		oeword 8615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
326	80, 323, 324, 325	mp3an2i 1462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
327	321, 326	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
328	163, 327	eqsstrrid 4029	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ⊆ (ω ↑o 𝑥))
329		ssequn1 4180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ (ω ↑o 𝑥) ↔ (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
330	328, 329	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
331	330	oveq1d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
332	241	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ∈ On)
333		oeoa 8622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
334	33, 323, 332, 333	mp3an2i 1462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
335		ssidd 4003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
336	322, 332, 335, 249	syl21anc 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
337	336	oveq2d 7440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
338	331, 334, 337	3eqtr2d 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
339	226, 228, 201	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
340	318, 338, 339	mpjaodan 956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
341	276	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
342	33, 228, 75	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o 𝑥) ∈ On)
343	342, 33	jctil 518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ∈ On ∧ (ω ↑o 𝑥) ∈ On))
344		onun2 6480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
345	226, 343, 344	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
346		omwordri 8597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ∪ (ω ↑o 𝑥)) ∈ On ∧ 𝐴 ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
347	345, 223, 236, 346	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
348	341, 347	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
349	340, 348	eqsstrrd 4019	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
350	255, 349	eqssd 3997	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
351	49	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
352	350, 351	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o 𝐵) = 𝐵)
353	352	ex 411	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
354	353	ad5antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
355	141, 143, 221, 354	mp3and 1460	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
356	355	ex 411	. . . . . . . . . . . 12 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
357	71, 356	syl5 34	. . . . . . . . . . 11 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
358	357	rexlimdva 3151	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → (∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
359	358	rexlimdva 3151	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
360	359	rexlimdva 3151	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
361	360	exlimdv 1928	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
362	70, 361	syl5 34	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
363	69, 362	mpd 15	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
364		eloni 6382	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
365	59, 364	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → Ord 𝐴)
366		ordtri2or 6470	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord ω) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
367	365, 158, 366	sylancl 584	. . . . 5 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
368	51, 363, 367	mpjaodan 956	. . . 4 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵)
369	368	ex 411	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = 𝐵))
370	6, 30, 369	3jaod 1425	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵))
371	370	imp 405	1 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∨ w3o 1083   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ∃!weu 2557   ≠ wne 2936  ∃wrex 3066   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947  ∅c0 4324  {cpr 4632  ⟨cotp 4638  Ord word 6371  Oncon0 6372  suc csuc 6374  (class class class)co 7424  ωcom 7874  1_oc1o 8484  2_oc2o 8485   +_o coa 8488   ·_o comu 8489   ↑_o coe 8490

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 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pr 5431  ax-un 7744  ax-reg 9621  ax-inf2 9670

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 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-ot 4639  df-uni 4911  df-int 4952  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-1st 7997  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-oadd 8495  df-omul 8496  df-oexp 8497

This theorem is referenced by:  omcl2  42765