Theorem omabs2 43921

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 2854	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅))
2		noel 4293	. . . . . . 7 ⊢ ¬ 𝐴 ∈ ∅
3	2	pm2.21i 120	. . . . . 6 ⊢ (𝐴 ∈ ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
4	1, 3	biimtrdi 256	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵)))
5	4	impd 415	. . . 4 ⊢ (𝐵 = ∅ → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
6	5	com12 33	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = 𝐵))
7		elpri 4609	. . . . . . . . 9 ⊢ (𝐴 ∈ {∅, 1o} → (𝐴 = ∅ ∨ 𝐴 = 1o))
8		eleq2 2854	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 ↔ ∅ ∈ ∅))
9		noel 4293	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ ∅
10	9	pm2.21i 120	. . . . . . . . . . 11 ⊢ (∅ ∈ ∅ → (𝐴 ·o 2o) = 2o)
11	8, 10	biimtrdi 256	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
12		oveq1 7407	. . . . . . . . . . . 12 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = (1o ·o 2o))
13		2on 8455	. . . . . . . . . . . . 13 ⊢ 2o ∈ On
14		om1r 8516	. . . . . . . . . . . . 13 ⊢ (2o ∈ On → (1o ·o 2o) = 2o)
15	13, 14	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1o ·o 2o) = 2o
16	12, 15	eqtrdi 2816	. . . . . . . . . . 11 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = 2o)
17	16	a1d 26	. . . . . . . . . 10 ⊢ (𝐴 = 1o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
18	11, 17	jaoi 870	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐴 = 1o) → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
19	7, 18	syl 18	. . . . . . . 8 ⊢ (𝐴 ∈ {∅, 1o} → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
20		df2o3 8449	. . . . . . . 8 ⊢ 2o = {∅, 1o}
21	19, 20	eleq2s 2883	. . . . . . 7 ⊢ (𝐴 ∈ 2o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
22	21	imp 411	. . . . . 6 ⊢ ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o)
23	22	a1i 11	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o))
24		eleq2 2854	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o))
25	24	anbi1d 642	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ∈ 2o ∧ ∅ ∈ 𝐴)))
26		oveq2 7408	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ·o 𝐵) = (𝐴 ·o 2o))
27		id 23	. . . . . 6 ⊢ (𝐵 = 2o → 𝐵 = 2o)
28	26, 27	eqeq12d 2781	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o 2o) = 2o))
29	23, 25, 28	3imtr4d 297	. . . 4 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
30	29	com12 33	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = 2o → (𝐴 ·o 𝐵) = 𝐵))
31		simpr 489	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → 𝐴 ∈ ω)
32		simpllr 787	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ 𝐴)
33		omelon 9603	. . . . . . . . . 10 ⊢ ω ∈ On
34		oecl 8510	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
35	33, 34	mpan 702	. . . . . . . . 9 ⊢ (𝐶 ∈ On → (ω ↑o 𝐶) ∈ On)
36	35	adantl 486	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
37	36	ad2antlr 739	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (ω ↑o 𝐶) ∈ On)
38	33	jctl 532	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 𝐶 ∈ On))
39		peano1 7873	. . . . . . . . . 10 ⊢ ∅ ∈ ω
40		oen0 8560	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
41	38, 39, 40	sylancl 597	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ∅ ∈ (ω ↑o 𝐶))
42	41	adantl 486	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ∅ ∈ (ω ↑o 𝐶))
43	42	ad2antlr 739	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
44		omabs 8625	. . . . . . 7 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ((ω ↑o 𝐶) ∈ On ∧ ∅ ∈ (ω ↑o 𝐶))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
45	31, 32, 37, 43, 44	syl22anc 851	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
46		oveq2 7408	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → (𝐴 ·o 𝐵) = (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
47		id 23	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
48	46, 47	eqeq12d 2781	. . . . . . . 8 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
49	48	adantr 485	. . . . . . 7 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
50	49	ad2antlr 739	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
51	45, 50	mpbird 260	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (𝐴 ·o 𝐵) = 𝐵)
52		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
53		oecl 8510	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
54	33, 35, 53	sylancr 598	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → (ω ↑o (ω ↑o 𝐶)) ∈ On)
55	54	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
56	52, 55	eqeltrd 2865	. . . . . . . . . . 11 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
57		simpl 487	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → 𝐴 ∈ 𝐵)
58		onelon 6375	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On)
59	56, 57, 58	syl2anr 608	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ On)
60		simplr 780	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ∅ ∈ 𝐴)
61		ondif1 8474	. . . . . . . . . 10 ⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
62	59, 60, 61	sylanbrc 594	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ (On ∖ 1o))
63		1onn 8614	. . . . . . . . . 10 ⊢ 1o ∈ ω
64		ondif2 8475	. . . . . . . . . 10 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
65	33, 63, 64	mpbir2an 723	. . . . . . . . 9 ⊢ ω ∈ (On ∖ 2o)
66	62, 65	jctil 528	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
67	66	adantr 485	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
68		oeeu 8577	. . . . . . 7 ⊢ ((ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)) → ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
69	67, 68	syl 18	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
70		euex 2607	. . . . . . 7 ⊢ (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
71		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
72		0ss 4357	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝑧
73		0elon 6405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
74		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
75		oecl 8510	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
76	33, 74, 75	sylancr 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
77	76	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → (ω ↑o 𝑥) ∈ On)
78		onelon 6375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
79	77, 78	sylancom 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
80		1on 8454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1o ∈ On
81		omcl 8509	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 1o ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
82	76, 80, 81	sylancl 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
83	82	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
84		oaword 8522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∅ ∈ On ∧ 𝑧 ∈ On ∧ ((ω ↑o 𝑥) ·o 1o) ∈ On) → (∅ ⊆ 𝑧 ↔ (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
85	84	biimpd 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∅ ∈ On ∧ 𝑧 ∈ On ∧ ((ω ↑o 𝑥) ·o 1o) ∈ On) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
86	73, 79, 83, 85	mp3an2ani 1492	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
87	72, 86	mpi 21	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧))
88		simpllr 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ (ω ∖ 1o))
89		omsson 7854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ω ⊆ On
90		ssdif 4100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ On → (ω ∖ 1o) ⊆ (On ∖ 1o))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ω ∖ 1o) ⊆ (On ∖ 1o)
92	91	sseli 3935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ (On ∖ 1o))
93		ondif1 8474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (On ∖ 1o) ↔ (𝑦 ∈ On ∧ ∅ ∈ 𝑦))
94		df-1o 8441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o = suc ∅
95		eloni 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → Ord 𝑦)
96		ordsucss 7802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑦 → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
97	95, 96	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
98	97	imp 411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → suc ∅ ⊆ 𝑦)
99	94, 98	eqsstrid 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → 1o ⊆ 𝑦)
100	93, 99	sylbi 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (On ∖ 1o) → 1o ⊆ 𝑦)
101	88, 92, 100	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑦)
102		eldifi 4087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ ω)
103		nnon 7856	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
104	102, 103	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ On)
105	104	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑦 ∈ On)
106		simp-4r 795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ On)
107	33, 106, 75	sylancr 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ On)
108		omwordi 8544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1o ∈ On ∧ 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
109	80, 105, 107, 108	mp3an2ani 1492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
110	101, 109	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦))
111	105	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ On)
112		omcl 8509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
113	107, 111, 112	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
114	79	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ On)
115		oawordri 8523	. . . . . . . . . . . . . . . . . . . 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 1394	. . . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
118	87, 117	sstrd 3949	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
119	33, 75	mpan 702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (ω ↑o 𝑥) ∈ On)
120	119, 80, 81	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) ∈ On)
121		oa0 8489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ω ↑o 𝑥) ·o 1o) ∈ On → (((ω ↑o 𝑥) ·o 1o) +o ∅) = ((ω ↑o 𝑥) ·o 1o))
122	120, 121	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → (((ω ↑o 𝑥) ·o 1o) +o ∅) = ((ω ↑o 𝑥) ·o 1o))
123		om1 8515	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ↑o 𝑥) ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
124	119, 123	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
125	122, 124	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ On → (((ω ↑o 𝑥) ·o 1o) +o ∅) = (ω ↑o 𝑥))
126	106, 125	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) = (ω ↑o 𝑥))
127		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
128	118, 126, 127	3sstr3d 3993	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ⊆ 𝐴)
129		simp-7l 800	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ 𝐵)
130		simplrl 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
131	130	ad4antr 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
132	129, 131	eleqtrd 2867	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
133	55	ad6antlr 749	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
134		ontr2 6398	. . . . . . . . . . . . . . . . 17 ⊢ (((ω ↑o 𝑥) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
135	107, 133, 134	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
136	128, 132, 135	mp2and 711	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶)))
137	36	ad6antlr 749	. . . . . . . . . . . . . . . 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 8562	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
140	106, 137, 138, 139	syl3anc 1394	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
141	136, 140	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ (ω ↑o 𝐶))
142		simp-5r 797	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ 𝐴)
143	142, 128	unssd 4147	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
144		simplr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ (ω ↑o 𝑥))
145		onelpss 6390	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) ↔ (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
146	145	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
147	79, 107, 146	syl2an2r 697	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
148	144, 147	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)))
149		simpl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)) → 𝑧 ⊆ (ω ↑o 𝑥))
150	148, 149	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ⊆ (ω ↑o 𝑥))
151		oaword 8522	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) ↔ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
152	151	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
153	114, 107, 113, 152	syl3anc 1394	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
154	150, 153	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
155		omsuc 8499	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
156	107, 111, 155	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
157	154, 156	sseqtrrd 3976	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o suc 𝑦))
158		ordom 7860	. . . . . . . . . . . . . . . . . . 19 ⊢ Ord ω
159	88, 102	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ ω)
160		ordsucss 7802	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ω → (𝑦 ∈ ω → suc 𝑦 ⊆ ω))
161	158, 159, 160	mpsyl 69	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ ω)
162		oe1 8517	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
163	33, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ↑o 1o) = ω
164		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑥 = ∅)
165	164	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = (ω ↑o ∅))
166		oe0 8495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ∈ On → (ω ↑o ∅) = 1o)
167	33, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) = 1o
168	165, 167	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = 1o)
169	168	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = (1o ·o 𝑦))
170	104	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → 𝑦 ∈ On)
171	170	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ On)
172		om1r 8516	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → (1o ·o 𝑦) = 𝑦)
173	171, 172	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (1o ·o 𝑦) = 𝑦)
174	169, 173	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = 𝑦)
175		simpllr 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ (ω ↑o 𝑥))
176	175, 168	eleqtrd 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ 1o)
177		el1o 8468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 1o ↔ 𝑧 = ∅)
178	176, 177	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 = ∅)
179	174, 178	oveq12d 7418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = (𝑦 +o ∅))
180		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
181		oa0 8489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ On → (𝑦 +o ∅) = 𝑦)
182	171, 181	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (𝑦 +o ∅) = 𝑦)
183	179, 180, 182	3eqtr3d 2808	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 = 𝑦)
184	159	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ ω)
185	183, 184	eqeltrd 2865	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 ∈ ω)
186	185	ex 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 𝐴 ∈ ω))
187	33, 33	pm3.2i 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ On ∧ ω ∈ On)
188		ontr2 6398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ ω ∈ On) → ((ω ⊆ 𝐴 ∧ 𝐴 ∈ ω) → ω ∈ ω))
189	188	expd 420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ ω ∈ On) → (ω ⊆ 𝐴 → (𝐴 ∈ ω → ω ∈ ω)))
190	187, 142, 189	mpsyl 69	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ∈ ω → ω ∈ ω))
191		ordirr 6368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord ω → ¬ ω ∈ ω)
192	158, 191	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ω ∈ ω
193	192	pm2.21i 120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ ω → 1o ⊆ 𝑥)
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∈ ω → 1o ⊆ 𝑥))
195	186, 190, 194	3syld 61	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 1o ⊆ 𝑥))
196		eloni 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → Ord 𝑥)
197		ordsucss 7802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
198	197	imp 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
199	94, 198	eqsstrid 3977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
200	199	ex 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
201	106, 196, 200	3syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
202		on0eqel 6475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
203	106, 202	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
204	195, 201, 203	mpjaod 873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑥)
205	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ∈ On)
206	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ∈ On)
207	205, 106, 206	3jca 1144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On))
208		oewordi 8565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
209	207, 39, 208	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
210	204, 209	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
211	163, 210	eqsstrrid 3978	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ (ω ↑o 𝑥))
212	161, 211	sstrd 3949	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ (ω ↑o 𝑥))
213		onsuc 7797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
214	111, 213	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ∈ On)
215		omwordi 8544	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
216	214, 107, 107, 215	syl3anc 1394	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
217	212, 216	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
218	157, 217	sstrd 3949	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
219	127	eqcomd 2771	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 = (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
220		oeoa 8571	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
221	33, 106, 106, 220	mp3an2i 1490	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
222	218, 219, 221	3sstr4d 3994	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
223		simpr3 1213	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
224	59	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ On)
225		simprr 784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐶 ∈ On)
226		simp1 1152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → 𝑥 ∈ (ω ↑o 𝐶))
227	225, 226	anim12i 624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)))
228		onelon 6375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
229	35, 228	sylan 591	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
230		pm4.24 573	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝑥 ∈ On))
231	229, 230	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 ∈ On ∧ 𝑥 ∈ On))
232		oacl 8508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On) → (𝑥 +o 𝑥) ∈ On)
233	231, 232	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 +o 𝑥) ∈ On)
234		oecl 8510	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
235	33, 233, 234	sylancr 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
236	227, 235	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
237	55	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
238		omwordri 8545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ (ω ↑o (𝑥 +o 𝑥)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
239	224, 236, 237, 238	syl3anc 1394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
240	223, 239	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
241	227, 231, 232	3syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o 𝑥) ∈ On)
242	36	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ∈ On)
243		oeoa 8571	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
244	33, 241, 242, 243	mp3an2i 1490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
245	227, 229	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ On)
246		oaass 8534	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
247	245, 245, 242, 246	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
248		simpr1 1211	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ (ω ↑o 𝐶))
249		ssidd 3962	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
250		oaabs2 8623	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ↑o 𝐶) ∈ On) ∧ (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶)) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
251	248, 242, 249, 250	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
252	251	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (𝑥 +o (ω ↑o 𝐶))) = (𝑥 +o (ω ↑o 𝐶)))
253	247, 252, 251	3eqtrd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
254	253	oveq2d 7416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
255	244, 254	eqtr3d 2802	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
256	240, 255	sseqtrd 3975	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (ω ↑o (ω ↑o 𝐶)))
257		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
258	257, 167	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = 1o)
259	258	uneq2d 4124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ∪ 1o))
260	33	oneluni 6470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ∈ ω → (ω ∪ 1o) = ω)
261	63, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ω ∪ 1o) = ω
262	261, 163	eqtr4i 2791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ω ∪ 1o) = (ω ↑o 1o)
263	259, 262	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
264	263	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
265	264	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
266	225	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → 𝐶 ∈ On)
267		oecl 8510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((ω ∈ On ∧ ∅ ∈ On) → (ω ↑o ∅) ∈ On)
268	33, 73, 267	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) ∈ On
269		oecl 8510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ∈ On ∧ (ω ↑o ∅) ∈ On) → (ω ↑o (ω ↑o ∅)) ∈ On)
270	33, 268, 269	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ω ↑o (ω ↑o ∅)) ∈ On
271	270	2a1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ On))
272	271, 54	jca2 522	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On)))
273	167	oveq2i 7411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ω ↑o (ω ↑o ∅)) = (ω ↑o 1o)
274	273, 163	eqtri 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ω ↑o (ω ↑o ∅)) = ω
275		ssun1 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ω ⊆ (ω ∪ (ω ↑o 𝑥))
276	274, 275	eqsstri 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ↑o (ω ↑o ∅)) ⊆ (ω ∪ (ω ↑o 𝑥))
277		simp2 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
278	276, 277	sstrid 3950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
279	278	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
280	57	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ 𝐵)
281		simplrl 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
282	280, 281	eleqtrd 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
283	279, 282	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
284	283	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
285		ontr2 6398	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
286	272, 284, 285	syl6ci 72	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
287		oeord 8562	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
288	73, 65, 287	mp3an13 1476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
289	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐶 ∈ On → ω ∈ (On ∖ 2o))
290		oeord 8562	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ω ↑o ∅) ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
291	268, 35, 289, 290	mp3an2i 1490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
292	288, 291	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
293	292	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶)) → ∅ ∈ 𝐶))
294	286, 293	sylcom 31	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ∅ ∈ 𝐶))
295		eloni 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → Ord 𝐶)
296		ordsucss 7802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶))
297	94	sseq1i 3967	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶)
298	296, 297	imbitrrdi 255	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
299	295, 298	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
300	294, 299	sylcom 31	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → 1o ⊆ 𝐶))
301	266, 300	jcai 525	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On ∧ 1o ⊆ 𝐶))
302	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → ω ∈ On)
303	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → 1o ∈ On)
304	302, 303, 35	3jca 1144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
305	304	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
306		oeoa 8571	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
307	305, 306	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
308	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → 1o ∈ ω)
309	35	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 𝐶) ∈ On)
310		oeword 8564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
311	80, 65, 310	mp3an13 1476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
312	311	biimpa 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 1o) ⊆ (ω ↑o 𝐶))
313	163, 312	eqsstrrid 3978	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ω ⊆ (ω ↑o 𝐶))
314		oaabs 8622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1o ∈ ω ∧ (ω ↑o 𝐶) ∈ On) ∧ ω ⊆ (ω ↑o 𝐶)) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
315	308, 309, 313, 314	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
316	315	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
317	307, 316	eqtr3d 2802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
318	301, 317	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
319	265, 318	eqtrd 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
320	245, 196, 197	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
321	320	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
322	94, 321	eqsstrid 3977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
323	248	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ (ω ↑o 𝐶))
324	242, 323, 228	syl2an2r 697	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ On)
325	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ∈ (On ∖ 2o))
326		oeword 8564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
327	80, 324, 325, 326	mp3an2i 1490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
328	322, 327	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
329	163, 328	eqsstrrid 3978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ⊆ (ω ↑o 𝑥))
330		ssequn1 4141	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ (ω ↑o 𝑥) ↔ (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
331	329, 330	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
332	331	oveq1d 7415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
333	242	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ∈ On)
334		oeoa 8571	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
335	33, 324, 333, 334	mp3an2i 1490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
336		ssidd 3962	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
337	323, 333, 336, 250	syl21anc 850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
338	337	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
339	332, 335, 338	3eqtr2d 2806	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
340	227, 229, 202	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
341	319, 339, 340	mpjaodan 973	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
342	277	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
343	33, 229, 75	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o 𝑥) ∈ On)
344	343, 33	jctil 528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ∈ On ∧ (ω ↑o 𝑥) ∈ On))
345		onun2 6460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
346	227, 344, 345	3syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
347		omwordri 8545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ∪ (ω ↑o 𝑥)) ∈ On ∧ 𝐴 ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
348	346, 224, 237, 347	syl3anc 1394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
349	342, 348	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
350	341, 349	eqsstrrd 3974	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
351	256, 350	eqssd 3956	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
352	49	ad2antlr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
353	351, 352	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o 𝐵) = 𝐵)
354	353	ex 417	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
355	354	ad5antr 746	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
356	141, 143, 222, 355	mp3and 1488	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
357	356	ex 417	. . . . . . . . . . . 12 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
358	71, 357	syl5 35	. . . . . . . . . . 11 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
359	358	rexlimdva 3166	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → (∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
360	359	rexlimdva 3166	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
361	360	rexlimdva 3166	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
362	361	exlimdv 1956	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
363	70, 362	syl5 35	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
364	69, 363	mpd 16	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
365		eloni 6360	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
366	59, 365	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → Ord 𝐴)
367		ordtri2or 6450	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord ω) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
368	366, 158, 367	sylancl 597	. . . . 5 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
369	51, 364, 368	mpjaodan 973	. . . 4 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵)
370	369	ex 417	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = 𝐵))
371	6, 30, 370	3jaod 1452	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵))
372	371	imp 411	1 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∨ w3o 1100   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∃!weu 2598   ≠ wne 2960  ∃wrex 3089   ∖ cdif 3904   ∪ cun 3905   ⊆ wss 3907  ∅c0 4288  {cpr 4587  ⟨cotp 4593  Ord word 6349  Oncon0 6350  suc csuc 6352  (class class class)co 7400  ωcom 7850  1_oc1o 8434  2_oc2o 8435   +_o coa 8438   ·_o comu 8439   ↑_o coe 8440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-inf2 9598

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-ot 4594  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-oadd 8445  df-omul 8446  df-oexp 8447

This theorem is referenced by:  omcl2  43922