Theorem omabs2 43760

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 2825	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅))
2		noel 4278	. . . . . . 7 ⊢ ¬ 𝐴 ∈ ∅
3	2	pm2.21i 119	. . . . . 6 ⊢ (𝐴 ∈ ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
4	1, 3	biimtrdi 253	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵)))
5	4	impd 410	. . . 4 ⊢ (𝐵 = ∅ → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
6	5	com12 32	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = 𝐵))
7		elpri 4591	. . . . . . . . 9 ⊢ (𝐴 ∈ {∅, 1o} → (𝐴 = ∅ ∨ 𝐴 = 1o))
8		eleq2 2825	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 ↔ ∅ ∈ ∅))
9		noel 4278	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ ∅
10	9	pm2.21i 119	. . . . . . . . . . 11 ⊢ (∅ ∈ ∅ → (𝐴 ·o 2o) = 2o)
11	8, 10	biimtrdi 253	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
12		oveq1 7374	. . . . . . . . . . . 12 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = (1o ·o 2o))
13		2on 8418	. . . . . . . . . . . . 13 ⊢ 2o ∈ On
14		om1r 8478	. . . . . . . . . . . . 13 ⊢ (2o ∈ On → (1o ·o 2o) = 2o)
15	13, 14	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1o ·o 2o) = 2o
16	12, 15	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = 2o)
17	16	a1d 25	. . . . . . . . . 10 ⊢ (𝐴 = 1o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
18	11, 17	jaoi 858	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ∨ 𝐴 = 1o) → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
19	7, 18	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ {∅, 1o} → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
20		df2o3 8413	. . . . . . . 8 ⊢ 2o = {∅, 1o}
21	19, 20	eleq2s 2854	. . . . . . 7 ⊢ (𝐴 ∈ 2o → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
22	21	imp 406	. . . . . 6 ⊢ ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o)
23	22	a1i 11	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 2o ∧ ∅ ∈ 𝐴) → (𝐴 ·o 2o) = 2o))
24		eleq2 2825	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o))
25	24	anbi1d 632	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ∈ 2o ∧ ∅ ∈ 𝐴)))
26		oveq2 7375	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ·o 𝐵) = (𝐴 ·o 2o))
27		id 22	. . . . . 6 ⊢ (𝐵 = 2o → 𝐵 = 2o)
28	26, 27	eqeq12d 2752	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o 2o) = 2o))
29	23, 25, 28	3imtr4d 294	. . . 4 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
30	29	com12 32	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = 2o → (𝐴 ·o 𝐵) = 𝐵))
31		simpr 484	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → 𝐴 ∈ ω)
32		simpllr 776	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ 𝐴)
33		omelon 9567	. . . . . . . . . 10 ⊢ ω ∈ On
34		oecl 8472	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
35	33, 34	mpan 691	. . . . . . . . 9 ⊢ (𝐶 ∈ On → (ω ↑o 𝐶) ∈ On)
36	35	adantl 481	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
37	36	ad2antlr 728	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (ω ↑o 𝐶) ∈ On)
38	33	jctl 523	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 𝐶 ∈ On))
39		peano1 7840	. . . . . . . . . 10 ⊢ ∅ ∈ ω
40		oen0 8522	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
41	38, 39, 40	sylancl 587	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ∅ ∈ (ω ↑o 𝐶))
42	41	adantl 481	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ∅ ∈ (ω ↑o 𝐶))
43	42	ad2antlr 728	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
44		omabs 8587	. . . . . . 7 ⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ ((ω ↑o 𝐶) ∈ On ∧ ∅ ∈ (ω ↑o 𝐶))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
45	31, 32, 37, 43, 44	syl22anc 839	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
46		oveq2 7375	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → (𝐴 ·o 𝐵) = (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
47		id 22	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
48	46, 47	eqeq12d 2752	. . . . . . . 8 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
49	48	adantr 480	. . . . . . 7 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
50	49	ad2antlr 728	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
51	45, 50	mpbird 257	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (𝐴 ·o 𝐵) = 𝐵)
52		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
53		oecl 8472	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
54	33, 35, 53	sylancr 588	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → (ω ↑o (ω ↑o 𝐶)) ∈ On)
55	54	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
56	52, 55	eqeltrd 2836	. . . . . . . . . . 11 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
57		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → 𝐴 ∈ 𝐵)
58		onelon 6348	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On)
59	56, 57, 58	syl2anr 598	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ On)
60		simplr 769	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ∅ ∈ 𝐴)
61		ondif1 8436	. . . . . . . . . 10 ⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
62	59, 60, 61	sylanbrc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ (On ∖ 1o))
63		1onn 8576	. . . . . . . . . 10 ⊢ 1o ∈ ω
64		ondif2 8437	. . . . . . . . . 10 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
65	33, 63, 64	mpbir2an 712	. . . . . . . . 9 ⊢ ω ∈ (On ∖ 2o)
66	62, 65	jctil 519	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
67	66	adantr 480	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)))
68		oeeu 8539	. . . . . . 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 2577	. . . . . . 7 ⊢ (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴))
71		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
72		0ss 4340	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝑧
73		0elon 6378	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
74		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
75		oecl 8472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
76	33, 74, 75	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
77	76	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → (ω ↑o 𝑥) ∈ On)
78		onelon 6348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
79	77, 78	sylancom 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
80		1on 8417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1o ∈ On
81		omcl 8471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 1o ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
82	76, 80, 81	sylancl 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
83	82	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
84		oaword 8484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∅ ∈ On ∧ 𝑧 ∈ On ∧ ((ω ↑o 𝑥) ·o 1o) ∈ On) → (∅ ⊆ 𝑧 ↔ (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
85	84	biimpd 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∅ ∈ On ∧ 𝑧 ∈ On ∧ ((ω ↑o 𝑥) ·o 1o) ∈ On) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 1o) +o 𝑧)))
86	73, 79, 83, 85	mp3an2ani 1471	. . . . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ (ω ∖ 1o))
89		omsson 7821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ω ⊆ On
90		ssdif 4084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ On → (ω ∖ 1o) ⊆ (On ∖ 1o))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ω ∖ 1o) ⊆ (On ∖ 1o)
92	91	sseli 3917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ (On ∖ 1o))
93		ondif1 8436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (On ∖ 1o) ↔ (𝑦 ∈ On ∧ ∅ ∈ 𝑦))
94		df-1o 8405	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o = suc ∅
95		eloni 6333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → Ord 𝑦)
96		ordsucss 7769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑦 → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
97	95, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
98	97	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → suc ∅ ⊆ 𝑦)
99	94, 98	eqsstrid 3960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → 1o ⊆ 𝑦)
100	93, 99	sylbi 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (On ∖ 1o) → 1o ⊆ 𝑦)
101	88, 92, 100	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑦)
102		eldifi 4071	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ ω)
103		nnon 7823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ On)
105	104	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑦 ∈ On)
106		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ On)
107	33, 106, 75	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ On)
108		omwordi 8506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1o ∈ On ∧ 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
109	80, 105, 107, 108	mp3an2ani 1471	. . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ On)
112		omcl 8471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
113	107, 111, 112	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
114	79	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ On)
115		oawordri 8485	. . . . . . . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . . . . . . 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 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
119	33, 75	mpan 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (ω ↑o 𝑥) ∈ On)
120	119, 80, 81	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) ∈ On)
121		oa0 8451	. . . . . . . . . . . . . . . . . . . 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 8477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ↑o 𝑥) ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
124	119, 123	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
125	122, 124	eqtrd 2771	. . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
128	118, 126, 127	3sstr3d 3976	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ⊆ 𝐴)
129		simp-7l 789	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ 𝐵)
130		simplrl 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
131	130	ad4antr 733	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
132	129, 131	eleqtrd 2838	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
133	55	ad6antlr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
134		ontr2 6371	. . . . . . . . . . . . . . . . 17 ⊢ (((ω ↑o 𝑥) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
135	107, 133, 134	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
136	128, 132, 135	mp2and 700	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶)))
137	36	ad6antlr 738	. . . . . . . . . . . . . . . 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 8524	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
140	106, 137, 138, 139	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
141	136, 140	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ (ω ↑o 𝐶))
142		simp-5r 786	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ 𝐴)
143	142, 128	unssd 4132	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
144		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ (ω ↑o 𝑥))
145		onelpss 6363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) ↔ (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
146	145	biimpd 229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
147	79, 107, 146	syl2an2r 686	. . . . . . . . . . . . . . . . . . . 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 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)) → 𝑧 ⊆ (ω ↑o 𝑥))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ⊆ (ω ↑o 𝑥))
151		oaword 8484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) ↔ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
152	151	biimpd 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥))))
153	114, 107, 113, 152	syl3anc 1374	. . . . . . . . . . . . . . . . . 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 8461	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
156	107, 111, 155	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
157	154, 156	sseqtrrd 3959	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o suc 𝑦))
158		ordom 7827	. . . . . . . . . . . . . . . . . . 19 ⊢ Ord ω
159	88, 102	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ ω)
160		ordsucss 7769	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ω → (𝑦 ∈ ω → suc 𝑦 ⊆ ω))
161	158, 159, 160	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ ω)
162		oe1 8479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
163	33, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (ω ↑o 1o) = ω
164		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑥 = ∅)
165	164	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = (ω ↑o ∅))
166		oe0 8457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ∈ On → (ω ↑o ∅) = 1o)
167	33, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) = 1o
168	165, 167	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = 1o)
169	168	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = (1o ·o 𝑦))
170	104	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → 𝑦 ∈ On)
171	170	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ On)
172		om1r 8478	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω ↑o 𝑥) ·o 𝑦) = 𝑦)
175		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ (ω ↑o 𝑥))
176	175, 168	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ 1o)
177		el1o 8430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 1o ↔ 𝑧 = ∅)
178	176, 177	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 = ∅)
179	174, 178	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = (𝑦 +o ∅))
180		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴)
181		oa0 8451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ On → (𝑦 +o ∅) = 𝑦)
182	171, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (𝑦 +o ∅) = 𝑦)
183	179, 180, 182	3eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 = 𝑦)
184	159	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ ω)
185	183, 184	eqeltrd 2836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 ∈ ω)
186	185	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 𝐴 ∈ ω))
187	33, 33	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ On ∧ ω ∈ On)
188		ontr2 6371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ ω ∈ On) → ((ω ⊆ 𝐴 ∧ 𝐴 ∈ ω) → ω ∈ ω))
189	188	expd 415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ ω ∈ On) → (ω ⊆ 𝐴 → (𝐴 ∈ ω → ω ∈ ω)))
190	187, 142, 189	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ∈ ω → ω ∈ ω))
191		ordirr 6341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord ω → ¬ ω ∈ ω)
192	158, 191	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ω ∈ ω
193	192	pm2.21i 119	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ ω → 1o ⊆ 𝑥)
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∈ ω → 1o ⊆ 𝑥))
195	186, 190, 194	3syld 60	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 1o ⊆ 𝑥))
196		eloni 6333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → Ord 𝑥)
197		ordsucss 7769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
198	197	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
199	94, 198	eqsstrid 3960	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
200	199	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
201	106, 196, 200	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
202		on0eqel 6448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
203	106, 202	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
204	195, 201, 203	mpjaod 861	. . . . . . . . . . . . . . . . . . . 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 1129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On))
208		oewordi 8527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
209	207, 39, 208	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
210	204, 209	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
211	163, 210	eqsstrrid 3961	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ (ω ↑o 𝑥))
212	161, 211	sstrd 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ (ω ↑o 𝑥))
213		onsuc 7764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
214	111, 213	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ∈ On)
215		omwordi 8506	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
216	214, 107, 107, 215	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
217	212, 216	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
218	157, 217	sstrd 3932	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
219	127	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 = (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
220		oeoa 8533	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
221	33, 106, 106, 220	mp3an2i 1469	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
222	218, 219, 221	3sstr4d 3977	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
223		simpr3 1198	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
224	59	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ On)
225		simprr 773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐶 ∈ On)
226		simp1 1137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → 𝑥 ∈ (ω ↑o 𝐶))
227	225, 226	anim12i 614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)))
228		onelon 6348	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
229	35, 228	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
230		pm4.24 563	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝑥 ∈ On))
231	229, 230	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 ∈ On ∧ 𝑥 ∈ On))
232		oacl 8470	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On) → (𝑥 +o 𝑥) ∈ On)
233	231, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 +o 𝑥) ∈ On)
234		oecl 8472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
235	33, 233, 234	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
236	227, 235	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
237	55	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
238		omwordri 8507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ (ω ↑o (𝑥 +o 𝑥)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
239	224, 236, 237, 238	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
240	223, 239	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
241	227, 231, 232	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o 𝑥) ∈ On)
242	36	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ∈ On)
243		oeoa 8533	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
244	33, 241, 242, 243	mp3an2i 1469	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
245	227, 229	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ On)
246		oaass 8496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
247	245, 245, 242, 246	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
248		simpr1 1196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ (ω ↑o 𝐶))
249		ssidd 3945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
250		oaabs2 8585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ↑o 𝐶) ∈ On) ∧ (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶)) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
251	248, 242, 249, 250	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
252	251	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (𝑥 +o (ω ↑o 𝐶))) = (𝑥 +o (ω ↑o 𝐶)))
253	247, 252, 251	3eqtrd 2775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
254	253	oveq2d 7383	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
255	244, 254	eqtr3d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
256	240, 255	sseqtrd 3958	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (ω ↑o (ω ↑o 𝐶)))
257		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
258	257, 167	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = 1o)
259	258	uneq2d 4108	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ∪ 1o))
260	33	oneluni 6443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ∈ ω → (ω ∪ 1o) = ω)
261	63, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ω ∪ 1o) = ω
262	261, 163	eqtr4i 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ω ∪ 1o) = (ω ↑o 1o)
263	259, 262	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
264	263	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
265	264	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
266	225	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → 𝐶 ∈ On)
267		oecl 8472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((ω ∈ On ∧ ∅ ∈ On) → (ω ↑o ∅) ∈ On)
268	33, 73, 267	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) ∈ On
269		oecl 8472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ∈ On ∧ (ω ↑o ∅) ∈ On) → (ω ↑o (ω ↑o ∅)) ∈ On)
270	33, 268, 269	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ω ↑o (ω ↑o ∅)) ∈ On
271	270	2a1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ On))
272	271, 54	jca2 513	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On)))
273	167	oveq2i 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ω ↑o (ω ↑o ∅)) = (ω ↑o 1o)
274	273, 163	eqtri 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ω ↑o (ω ↑o ∅)) = ω
275		ssun1 4118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ω ⊆ (ω ∪ (ω ↑o 𝑥))
276	274, 275	eqsstri 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ↑o (ω ↑o ∅)) ⊆ (ω ∪ (ω ↑o 𝑥))
277		simp2 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
278	276, 277	sstrid 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
279	278	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
280	57	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ 𝐵)
281		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
282	280, 281	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
283	279, 282	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
284	283	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
285		ontr2 6371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
286	272, 284, 285	syl6ci 71	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
287		oeord 8524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
288	73, 65, 287	mp3an13 1455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
289	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐶 ∈ On → ω ∈ (On ∖ 2o))
290		oeord 8524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ω ↑o ∅) ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
291	268, 35, 289, 290	mp3an2i 1469	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
292	288, 291	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
293	292	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶)) → ∅ ∈ 𝐶))
294	286, 293	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ∅ ∈ 𝐶))
295		eloni 6333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → Ord 𝐶)
296		ordsucss 7769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶))
297	94	sseq1i 3950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶)
298	296, 297	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
299	295, 298	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
300	294, 299	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → 1o ⊆ 𝐶))
301	266, 300	jcai 516	. . . . . . . . . . . . . . . . . . . . . 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 1129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
305	304	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
306		oeoa 8533	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
307	305, 306	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
308	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → 1o ∈ ω)
309	35	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 𝐶) ∈ On)
310		oeword 8526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
311	80, 65, 310	mp3an13 1455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
312	311	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 1o) ⊆ (ω ↑o 𝐶))
313	163, 312	eqsstrrid 3961	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ω ⊆ (ω ↑o 𝐶))
314		oaabs 8584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1o ∈ ω ∧ (ω ↑o 𝐶) ∈ On) ∧ ω ⊆ (ω ↑o 𝐶)) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
315	308, 309, 313, 314	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
316	315	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
317	307, 316	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
318	301, 317	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
319	265, 318	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
320	245, 196, 197	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
321	320	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
322	94, 321	eqsstrid 3960	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
323	248	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ (ω ↑o 𝐶))
324	242, 323, 228	syl2an2r 686	. . . . . . . . . . . . . . . . . . . . . . . . . 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 8526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
327	80, 324, 325, 326	mp3an2i 1469	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
328	322, 327	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
329	163, 328	eqsstrrid 3961	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ⊆ (ω ↑o 𝑥))
330		ssequn1 4126	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ (ω ↑o 𝑥) ↔ (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
331	329, 330	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
332	331	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
333	242	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ∈ On)
334		oeoa 8533	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
335	33, 324, 333, 334	mp3an2i 1469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
336		ssidd 3945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
337	323, 333, 336, 250	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
338	337	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
339	332, 335, 338	3eqtr2d 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
340	227, 229, 202	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
341	319, 339, 340	mpjaodan 961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
342	277	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
343	33, 229, 75	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o 𝑥) ∈ On)
344	343, 33	jctil 519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ∈ On ∧ (ω ↑o 𝑥) ∈ On))
345		onun2 6433	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
346	227, 344, 345	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
347		omwordri 8507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ∪ (ω ↑o 𝑥)) ∈ On ∧ 𝐴 ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
348	346, 224, 237, 347	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
349	342, 348	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
350	341, 349	eqsstrrd 3957	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
351	256, 350	eqssd 3939	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
352	49	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
353	351, 352	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o 𝐵) = 𝐵)
354	353	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
355	354	ad5antr 735	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
356	141, 143, 222, 355	mp3and 1467	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
357	356	ex 412	. . . . . . . . . . . 12 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
358	71, 357	syl5 34	. . . . . . . . . . 11 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
359	358	rexlimdva 3138	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → (∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
360	359	rexlimdva 3138	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
361	360	rexlimdva 3138	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
362	361	exlimdv 1935	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
363	70, 362	syl5 34	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
364	69, 363	mpd 15	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
365		eloni 6333	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
366	59, 365	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → Ord 𝐴)
367		ordtri2or 6423	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord ω) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
368	366, 158, 367	sylancl 587	. . . . 5 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
369	51, 364, 368	mpjaodan 961	. . . 4 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵)
370	369	ex 412	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = 𝐵))
371	6, 30, 370	3jaod 1432	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵))
372	371	imp 406	1 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃!weu 2568   ≠ wne 2932  ∃wrex 3061   ∖ cdif 3886   ∪ cun 3887   ⊆ wss 3889  ∅c0 4273  {cpr 4569  ⟨cotp 4575  Ord word 6322  Oncon0 6323  suc csuc 6325  (class class class)co 7367  ωcom 7817  1_oc1o 8398  2_oc2o 8399   +_o coa 8402   ·_o comu 8403   ↑_o coe 8404

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-ot 4576  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-oadd 8409  df-omul 8410  df-oexp 8411

This theorem is referenced by:  omcl2  43761