Theorem omabs2 42067

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 2822	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅))
2		noel 4329	. . . . . . 7 ⊢ ¬ 𝐴 ∈ ∅
3	2	pm2.21i 119	. . . . . 6 ⊢ (𝐴 ∈ ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
4	1, 3	syl6bi 252	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵)))
5	4	impd 411	. . . 4 ⊢ (𝐵 = ∅ → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
6	5	com12 32	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = 𝐵))
7		elpri 4649	. . . . . . . . 9 ⊢ (𝐴 ∈ {∅, 1o} → (𝐴 = ∅ ∨ 𝐴 = 1o))
8		eleq2 2822	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 ↔ ∅ ∈ ∅))
9		noel 4329	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ ∅
10	9	pm2.21i 119	. . . . . . . . . . 11 ⊢ (∅ ∈ ∅ → (𝐴 ·o 2o) = 2o)
11	8, 10	syl6bi 252	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
12		oveq1 7412	. . . . . . . . . . . 12 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = (1o ·o 2o))
13		2on 8476	. . . . . . . . . . . . 13 ⊢ 2o ∈ On
14		om1r 8539	. . . . . . . . . . . . 13 ⊢ (2o ∈ On → (1o ·o 2o) = 2o)
15	13, 14	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1o ·o 2o) = 2o
16	12, 15	eqtrdi 2788	. . . . . . . . . . 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 8470	. . . . . . . 8 ⊢ 2o = {∅, 1o}
21	19, 20	eleq2s 2851	. . . . . . 7 ⊢ (𝐴 ∈ 2o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
22	21	imp 407	. . . . . 6 ⊢ ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o)
23	22	a1i 11	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o))
24		eleq2 2822	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o))
25	24	anbi1d 630	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ∈ 2o ∧ ∅ ∈ 𝐴)))
26		oveq2 7413	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ·o 𝐵) = (𝐴 ·o 2o))
27		id 22	. . . . . 6 ⊢ (𝐵 = 2o → 𝐵 = 2o)
28	26, 27	eqeq12d 2748	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o 2o) = 2o))
29	23, 25, 28	3imtr4d 293	. . . 4 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
30	29	com12 32	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = 2o → (𝐴 ·o 𝐵) = 𝐵))
31		simpr 485	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → 𝐴 ∈ ω)
32		simpllr 774	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ 𝐴)
33		omelon 9637	. . . . . . . . . 10 ⊢ ω ∈ On
34		oecl 8533	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
35	33, 34	mpan 688	. . . . . . . . 9 ⊢ (𝐶 ∈ On → (ω ↑o 𝐶) ∈ On)
36	35	adantl 482	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
37	36	ad2antlr 725	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (ω ↑o 𝐶) ∈ On)
38	33	jctl 524	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 𝐶 ∈ On))
39		peano1 7875	. . . . . . . . . 10 ⊢ ∅ ∈ ω
40		oen0 8582	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
41	38, 39, 40	sylancl 586	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ∅ ∈ (ω ↑o 𝐶))
42	41	adantl 482	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ∅ ∈ (ω ↑o 𝐶))
43	42	ad2antlr 725	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
44		omabs 8646	. . . . . . 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 7413	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → (𝐴 ·o 𝐵) = (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
47		id 22	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
48	46, 47	eqeq12d 2748	. . . . . . . 8 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
49	48	adantr 481	. . . . . . 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 483	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
53		oecl 8533	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
54	33, 35, 53	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → (ω ↑o (ω ↑o 𝐶)) ∈ On)
55	54	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
56	52, 55	eqeltrd 2833	. . . . . . . . . . 11 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
57		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → 𝐴 ∈ 𝐵)
58		onelon 6386	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On)
59	56, 57, 58	syl2anr 597	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ On)
60		simplr 767	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ∅ ∈ 𝐴)
61		ondif1 8497	. . . . . . . . . 10 ⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
62	59, 60, 61	sylanbrc 583	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ (On ∖ 1o))
63		1onn 8635	. . . . . . . . . 10 ⊢ 1o ∈ ω
64		ondif2 8498	. . . . . . . . . 10 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
65	33, 63, 64	mpbir2an 709	. . . . . . . . 9 ⊢ ω ∈ (On ∖ 2o)
66	62, 65	jctil 520	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
67	66	adantr 481	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
68		oeeu 8599	. . . . . . 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 2571	. . . . . . 7 ⊢ (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
71		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
72		0ss 4395	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝑧
73		0elon 6415	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
74		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
75		oecl 8533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
76	33, 74, 75	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
77	76	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → (ω ↑o 𝑥) ∈ On)
78		onelon 6386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
79	77, 78	sylancom 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
80		1on 8474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1o ∈ On
81		omcl 8532	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 1o ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
82	76, 80, 81	sylancl 586	. . . . . . . . . . . . . . . . . . . . 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 8545	. . . . . . . . . . . . . . . . . . . . 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 1468	. . . . . . . . . . . . . . . . . . 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 7855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ω ⊆ On
90		ssdif 4138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ On → (ω ∖ 1o) ⊆ (On ∖ 1o))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ω ∖ 1o) ⊆ (On ∖ 1o)
92	91	sseli 3977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ (On ∖ 1o))
93		ondif1 8497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (On ∖ 1o) ↔ (𝑦 ∈ On ∧ ∅ ∈ 𝑦))
94		df-1o 8462	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o = suc ∅
95		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → Ord 𝑦)
96		ordsucss 7802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑦 → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
97	95, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
98	97	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → suc ∅ ⊆ 𝑦)
99	94, 98	eqsstrid 4029	. . . . . . . . . . . . . . . . . . . . . 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 7857	. . . . . . . . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ On)
108		omwordi 8567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1o ∈ On ∧ 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
109	80, 105, 107, 108	mp3an2ani 1468	. . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ On)
112		omcl 8532	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
113	107, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
114	79	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ On)
115		oawordri 8546	. . . . . . . . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . . . . . . . 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 3991	. . . . . . . . . . . . . . . . 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 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) ∈ On)
121		oa0 8512	. . . . . . . . . . . . . . . . . . . 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 8538	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ↑o 𝑥) ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
124	119, 123	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
125	122, 124	eqtrd 2772	. . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
128	118, 126, 127	3sstr3d 4027	. . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . . . 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 6408	. . . . . . . . . . . . . . . . 17 ⊢ (((ω ↑o 𝑥) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
135	107, 133, 134	syl2anc 584	. . . . . . . . . . . . . . . 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 8584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
140	106, 137, 138, 139	syl3anc 1371	. . . . . . . . . . . . . . 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 4185	. . . . . . . . . . . . . 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 6401	. . . . . . . . . . . . . . . . . . . . . 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 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)) → 𝑧 ⊆ (ω ↑o 𝑥))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ⊆ (ω ↑o 𝑥))
151		oaword 8545	. . . . . . . . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . . . . . . 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 8522	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
156	107, 111, 155	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
157	154, 156	sseqtrrd 4022	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o suc 𝑦))
158		ordom 7861	. . . . . . . . . . . . . . . . . . 19 ⊢ Ord ω
159	88, 102	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ ω)
160		ordsucss 7802	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ω → (𝑦 ∈ ω → suc 𝑦 ⊆ ω))
161	158, 159, 160	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ ω)
162		oe1 8540	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
163	33, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ↑o 1o) = ω
164		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑥 = ∅)
165	164	oveq2d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = (ω ↑o ∅))
166		oe0 8518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ∈ On → (ω ↑o ∅) = 1o)
167	33, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) = 1o
168	165, 167	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = 1o)
169	168	oveq1d 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = (1o ·o 𝑦))
170	104	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → 𝑦 ∈ On)
171	170	ad5ant12 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ On)
172		om1r 8539	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ 1o)
177		el1o 8491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 1o ↔ 𝑧 = ∅)
178	176, 177	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 = ∅)
179	174, 178	oveq12d 7423	. . . . . . . . . . . . . . . . . . . . . . . . 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 8512	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ On → (𝑦 +o ∅) = 𝑦)
182	171, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (𝑦 +o ∅) = 𝑦)
183	179, 180, 182	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 = 𝑦)
184	159	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ ω)
185	183, 184	eqeltrd 2833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 ∈ ω)
186	185	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 𝐴 ∈ ω))
187	33, 33	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ On ∧ ω ∈ On)
188		ontr2 6408	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ ω ∈ On) → ((ω ⊆ 𝐴 ∧ 𝐴 ∈ ω) → ω ∈ ω))
189	188	expd 416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ ω ∈ On) → (ω ⊆ 𝐴 → (𝐴 ∈ ω → ω ∈ ω)))
190	187, 142, 189	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ∈ ω → ω ∈ ω))
191		elirr 9588	. . . . . . . . . . . . . . . . . . . . . . . 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 6371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → Ord 𝑥)
196		ordsucss 7802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
197	196	imp 407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
198	94, 197	eqsstrid 4029	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
199	198	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
200	106, 195, 199	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
201		on0eqel 6485	. . . . . . . . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On))
207		oewordi 8587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
208	206, 39, 207	sylancl 586	. . . . . . . . . . . . . . . . . . . 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 4030	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ (ω ↑o 𝑥))
211	161, 210	sstrd 3991	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ (ω ↑o 𝑥))
212		onsuc 7795	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
213	111, 212	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ∈ On)
214		omwordi 8567	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
215	213, 107, 107, 214	syl3anc 1371	. . . . . . . . . . . . . . . . 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 3991	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
218	127	eqcomd 2738	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 = (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
219		oeoa 8593	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
220	33, 106, 106, 219	mp3an2i 1466	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
221	217, 218, 220	3sstr4d 4028	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
222		simpr3 1196	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
223	59	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ On)
224		simprr 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐶 ∈ On)
225		simp1 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → 𝑥 ∈ (ω ↑o 𝐶))
226	224, 225	anim12i 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)))
227		onelon 6386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
228	35, 227	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
229		pm4.24 564	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝑥 ∈ On))
230	228, 229	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 ∈ On ∧ 𝑥 ∈ On))
231		oacl 8531	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On) → (𝑥 +o 𝑥) ∈ On)
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 +o 𝑥) ∈ On)
233		oecl 8533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
234	33, 232, 233	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 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 8568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ (ω ↑o (𝑥 +o 𝑥)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
238	223, 235, 236, 237	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 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 8593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
243	33, 240, 241, 242	mp3an2i 1466	. . . . . . . . . . . . . . . . . . . 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 8557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
246	244, 244, 241, 245	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
247		simpr1 1194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ (ω ↑o 𝐶))
248		ssidd 4004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
249		oaabs2 8644	. . . . . . . . . . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (𝑥 +o (ω ↑o 𝐶))) = (𝑥 +o (ω ↑o 𝐶)))
252	246, 251, 250	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
253	252	oveq2d 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
254	243, 253	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
255	239, 254	sseqtrd 4021	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (ω ↑o (ω ↑o 𝐶)))
256		oveq2 7413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
257	256, 167	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = 1o)
258	257	uneq2d 4162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ∪ 1o))
259	33	oneluni 6480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ∈ ω → (ω ∪ 1o) = ω)
260	63, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ω ∪ 1o) = ω
261	260, 163	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ω ∪ 1o) = (ω ↑o 1o)
262	258, 261	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
263	262	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
264	263	oveq1d 7420	. . . . . . . . . . . . . . . . . . . . 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 8533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((ω ∈ On ∧ ∅ ∈ On) → (ω ↑o ∅) ∈ On)
267	33, 73, 266	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) ∈ On
268		oecl 8533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On)))
272	167	oveq2i 7416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ω ↑o (ω ↑o ∅)) = (ω ↑o 1o)
273	272, 163	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ω ↑o (ω ↑o ∅)) = ω
274		ssun1 4171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ω ⊆ (ω ∪ (ω ↑o 𝑥))
275	273, 274	eqsstri 4015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ↑o (ω ↑o ∅)) ⊆ (ω ∪ (ω ↑o 𝑥))
276		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
277	275, 276	sstrid 3992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
278	277	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
282	278, 281	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
283	282	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
284		ontr2 6408	. . . . . . . . . . . . . . . . . . . . . . . . . 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 8584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
287	73, 65, 286	mp3an13 1452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
288	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐶 ∈ On → ω ∈ (On ∖ 2o))
289		oeord 8584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ω ↑o ∅) ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
290	267, 35, 288, 289	mp3an2i 1466	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → Ord 𝐶)
295		ordsucss 7802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶))
296	94	sseq1i 4009	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶)
297	295, 296	syl6ibr 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 517	. . . . . . . . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
304	303	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
305		oeoa 8593	. . . . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 𝐶) ∈ On)
309		oeword 8586	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
310	80, 65, 309	mp3an13 1452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
311	310	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 1o) ⊆ (ω ↑o 𝐶))
312	163, 311	eqsstrrid 4030	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ω ⊆ (ω ↑o 𝐶))
313		oaabs 8643	. . . . . . . . . . . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
316	306, 315	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
321	94, 320	eqsstrid 4029	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
322	247	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 8586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
326	80, 323, 324, 325	mp3an2i 1466	. . . . . . . . . . . . . . . . . . . . . . . . 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 4030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ⊆ (ω ↑o 𝑥))
329		ssequn1 4179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ (ω ↑o 𝑥) ↔ (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
330	328, 329	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
331	330	oveq1d 7420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
332	241	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ∈ On)
333		oeoa 8593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
334	33, 323, 332, 333	mp3an2i 1466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
335		ssidd 4004	. . . . . . . . . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
338	331, 334, 337	3eqtr2d 2778	. . . . . . . . . . . . . . . . . . . 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 957	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
341	276	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
342	33, 228, 75	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o 𝑥) ∈ On)
343	342, 33	jctil 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ∈ On ∧ (ω ↑o 𝑥) ∈ On))
344		onun2 6469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
345	226, 343, 344	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
346		omwordri 8568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ∪ (ω ↑o 𝑥)) ∈ On ∧ 𝐴 ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
347	345, 223, 236, 346	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 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 4020	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
350	255, 349	eqssd 3998	. . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . 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 1464	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
356	355	ex 413	. . . . . . . . . . . 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 3155	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → (∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
359	358	rexlimdva 3155	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
360	359	rexlimdva 3155	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
361	360	exlimdv 1936	. . . . . . 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 6371	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
365	59, 364	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → Ord 𝐴)
366		ordtri2or 6459	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord ω) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
367	365, 158, 366	sylancl 586	. . . . 5 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
368	51, 363, 367	mpjaodan 957	. . . 4 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵)
369	368	ex 413	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = 𝐵))
370	6, 30, 369	3jaod 1428	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵))
371	370	imp 407	1 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∃!weu 2562   ≠ wne 2940  ∃wrex 3070   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947  ∅c0 4321  {cpr 4629  ⟨cotp 4635  Ord word 6360  Oncon0 6361  suc csuc 6363  (class class class)co 7405  ωcom 7851  1_oc1o 8455  2_oc2o 8456   +_o coa 8459   ·_o comu 8460   ↑_o coe 8461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721  ax-reg 9583  ax-inf2 9632

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-oexp 8468

This theorem is referenced by:  omcl2  42068