Theorem omabs2 43345

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 2830	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅))
2		noel 4338	. . . . . . 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 4649	. . . . . . . . 9 ⊢ (𝐴 ∈ {∅, 1o} → (𝐴 = ∅ ∨ 𝐴 = 1o))
8		eleq2 2830	. . . . . . . . . . 11 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 ↔ ∅ ∈ ∅))
9		noel 4338	. . . . . . . . . . . 12 ⊢ ¬ ∅ ∈ ∅
10	9	pm2.21i 119	. . . . . . . . . . 11 ⊢ (∅ ∈ ∅ → (𝐴 ·o 2o) = 2o)
11	8, 10	biimtrdi 253	. . . . . . . . . 10 ⊢ (𝐴 = ∅ → (∅ ∈ 𝐴 → (𝐴 ·o 2o) = 2o))
12		oveq1 7438	. . . . . . . . . . . 12 ⊢ (𝐴 = 1o → (𝐴 ·o 2o) = (1o ·o 2o))
13		2on 8520	. . . . . . . . . . . . 13 ⊢ 2o ∈ On
14		om1r 8581	. . . . . . . . . . . . 13 ⊢ (2o ∈ On → (1o ·o 2o) = 2o)
15	13, 14	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1o ·o 2o) = 2o
16	12, 15	eqtrdi 2793	. . . . . . . . . . 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 8514	. . . . . . . 8 ⊢ 2o = {∅, 1o}
21	19, 20	eleq2s 2859	. . . . . . 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 2830	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o))
25	24	anbi1d 631	. . . . 5 ⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ∈ 2o ∧ ∅ ∈ 𝐴)))
26		oveq2 7439	. . . . . 6 ⊢ (𝐵 = 2o → (𝐴 ·o 𝐵) = (𝐴 ·o 2o))
27		id 22	. . . . . 6 ⊢ (𝐵 = 2o → 𝐵 = 2o)
28	26, 27	eqeq12d 2753	. . . . 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 9686	. . . . . . . . . 10 ⊢ ω ∈ On
34		oecl 8575	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
35	33, 34	mpan 690	. . . . . . . . 9 ⊢ (𝐶 ∈ On → (ω ↑o 𝐶) ∈ On)
36	35	adantl 481	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o 𝐶) ∈ On)
37	36	ad2antlr 727	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → (ω ↑o 𝐶) ∈ On)
38	33	jctl 523	. . . . . . . . . 10 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 𝐶 ∈ On))
39		peano1 7910	. . . . . . . . . 10 ⊢ ∅ ∈ ω
40		oen0 8624	. . . . . . . . . 10 ⊢ (((ω ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
41	38, 39, 40	sylancl 586	. . . . . . . . 9 ⊢ (𝐶 ∈ On → ∅ ∈ (ω ↑o 𝐶))
42	41	adantl 481	. . . . . . . 8 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ∅ ∈ (ω ↑o 𝐶))
43	42	ad2antlr 727	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ 𝐴 ∈ ω) → ∅ ∈ (ω ↑o 𝐶))
44		omabs 8689	. . . . . . 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 7439	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → (𝐴 ·o 𝐵) = (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
47		id 22	. . . . . . . . 9 ⊢ (𝐵 = (ω ↑o (ω ↑o 𝐶)) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
48	46, 47	eqeq12d 2753	. . . . . . . 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 727	. . . . . 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 8575	. . . . . . . . . . . . . 14 ⊢ ((ω ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
54	33, 35, 53	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ On → (ω ↑o (ω ↑o 𝐶)) ∈ On)
55	54	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
56	52, 55	eqeltrd 2841	. . . . . . . . . . 11 ⊢ ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
57		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → 𝐴 ∈ 𝐵)
58		onelon 6409	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On)
59	56, 57, 58	syl2anr 597	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ On)
60		simplr 769	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ∅ ∈ 𝐴)
61		ondif1 8539	. . . . . . . . . 10 ⊢ (𝐴 ∈ (On ∖ 1o) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴))
62	59, 60, 61	sylanbrc 583	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐴 ∈ (On ∖ 1o))
63		1onn 8678	. . . . . . . . . 10 ⊢ 1o ∈ ω
64		ondif2 8540	. . . . . . . . . 10 ⊢ (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
65	33, 63, 64	mpbir2an 711	. . . . . . . . 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 8641	. . . . . . 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 4400	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝑧
73		0elon 6438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ On
74		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → 𝑥 ∈ On)
75		oecl 8575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
76	33, 74, 75	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (ω ↑o 𝑥) ∈ On)
77	76	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → (ω ↑o 𝑥) ∈ On)
78		onelon 6409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
79	77, 78	sylancom 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On)
80		1on 8518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1o ∈ On
81		omcl 8574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 1o ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
82	76, 80, 81	sylancl 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
83	82	ad5ant12 756	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 1o) ∈ On)
84		oaword 8587	. . . . . . . . . . . . . . . . . . . . 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 1470	. . . . . . . . . . . . . . . . . . 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 7891	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ω ⊆ On
90		ssdif 4144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ On → (ω ∖ 1o) ⊆ (On ∖ 1o))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ω ∖ 1o) ⊆ (On ∖ 1o)
92	91	sseli 3979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ (On ∖ 1o))
93		ondif1 8539	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (On ∖ 1o) ↔ (𝑦 ∈ On ∧ ∅ ∈ 𝑦))
94		df-1o 8506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1o = suc ∅
95		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On → Ord 𝑦)
96		ordsucss 7838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑦 → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
97	95, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (∅ ∈ 𝑦 → suc ∅ ⊆ 𝑦))
98	97	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ On ∧ ∅ ∈ 𝑦) → suc ∅ ⊆ 𝑦)
99	94, 98	eqsstrid 4022	. . . . . . . . . . . . . . . . . . . . . 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 4131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ ω)
103		nnon 7893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (ω ∖ 1o) → 𝑦 ∈ On)
105	104	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ On)
108		omwordi 8609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1o ∈ On ∧ 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (1o ⊆ 𝑦 → ((ω ↑o 𝑥) ·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)))
109	80, 105, 107, 108	mp3an2ani 1470	. . . . . . . . . . . . . . . . . . . 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 8574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
113	107, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On)
114	79	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ On)
115		oawordri 8588	. . . . . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . . . . 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 3994	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 1o) +o ∅) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
119	33, 75	mpan 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ On → (ω ↑o 𝑥) ∈ On)
120	119, 80, 81	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) ∈ On)
121		oa0 8554	. . . . . . . . . . . . . . . . . . . 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 8580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ω ↑o 𝑥) ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
124	119, 123	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ On → ((ω ↑o 𝑥) ·o 1o) = (ω ↑o 𝑥))
125	122, 124	eqtrd 2777	. . . . . . . . . . . . . . . . . 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 4038	. . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
132	129, 131	eleqtrd 2843	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
133	55	ad6antlr 737	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
134		ontr2 6431	. . . . . . . . . . . . . . . . 17 ⊢ (((ω ↑o 𝑥) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
135	107, 133, 134	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
136	128, 132, 135	mp2and 699	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶)))
137	36	ad6antlr 737	. . . . . . . . . . . . . . . 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 8626	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω ↑o 𝐶))))
140	106, 137, 138, 139	syl3anc 1373	. . . . . . . . . . . . . . 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 4192	. . . . . . . . . . . . . 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 6424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) ↔ (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
146	145	biimpd 229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))))
147	79, 107, 146	syl2an2r 685	. . . . . . . . . . . . . . . . . . . 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 8587	. . . . . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . . . 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 8564	. . . . . . . . . . . . . . . . . 18 ⊢ (((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
156	107, 111, 155	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o 𝑥)))
157	154, 156	sseqtrrd 4021	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o suc 𝑦))
158		ordom 7897	. . . . . . . . . . . . . . . . . . 19 ⊢ Ord ω
159	88, 102	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ ω)
160		ordsucss 7838	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord ω → (𝑦 ∈ ω → suc 𝑦 ⊆ ω))
161	158, 159, 160	mpsyl 68	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ ω)
162		oe1 8582	. . . . . . . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = (ω ↑o ∅))
166		oe0 8560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ∈ On → (ω ↑o ∅) = 1o)
167	33, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) = 1o
168	165, 167	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω ↑o 𝑥) = 1o)
169	168	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . 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	ad5ant12 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ On)
172		om1r 8581	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ 1o)
177		el1o 8533	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 1o ↔ 𝑧 = ∅)
178	176, 177	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 = ∅)
179	174, 178	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . . . . 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 8554	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ On → (𝑦 +o ∅) = 𝑦)
182	171, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (𝑦 +o ∅) = 𝑦)
183	179, 180, 182	3eqtr3d 2785	. . . . . . . . . . . . . . . . . . . . . . . 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 2841	. . . . . . . . . . . . . . . . . . . . . . 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 6431	. . . . . . . . . . . . . . . . . . . . . . . 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		elirr 9637	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ ω ∈ ω
192	191	pm2.21i 119	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ∈ ω → 1o ⊆ 𝑥)
193	192	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∈ ω → 1o ⊆ 𝑥))
194	186, 190, 193	3syld 60	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 1o ⊆ 𝑥))
195		eloni 6394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → Ord 𝑥)
196		ordsucss 7838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
197	196	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
198	94, 197	eqsstrid 4022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Ord 𝑥 ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
199	198	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord 𝑥 → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
200	106, 195, 199	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ∈ 𝑥 → 1o ⊆ 𝑥))
201		on0eqel 6508	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
202	106, 201	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
203	194, 200, 202	mpjaod 861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑥)
204	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ∈ On)
205	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ∈ On)
206	204, 106, 205	3jca 1129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On))
207		oewordi 8629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On) ∧ ∅ ∈ ω) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
208	206, 39, 207	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑥 → (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
209	203, 208	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
210	163, 209	eqsstrrid 4023	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ (ω ↑o 𝑥))
211	161, 210	sstrd 3994	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ (ω ↑o 𝑥))
212		onsuc 7831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
213	111, 212	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ∈ On)
214		omwordi 8609	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑦 ∈ On ∧ (ω ↑o 𝑥) ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
215	213, 107, 107, 214	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥))))
216	211, 215	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
217	157, 216	sstrd 3994	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
218	127	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 = (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))
219		oeoa 8635	. . . . . . . . . . . . . . . 16 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ∈ On) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
220	33, 106, 106, 219	mp3an2i 1468	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω ↑o 𝑥)))
221	217, 218, 220	3sstr4d 4039	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
222		simpr3 1197	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))
223	59	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ On)
224		simprr 773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → 𝐶 ∈ On)
225		simp1 1137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → 𝑥 ∈ (ω ↑o 𝐶))
226	224, 225	anim12i 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)))
227		onelon 6409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
228	35, 227	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On)
229		pm4.24 563	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝑥 ∈ On))
230	228, 229	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 ∈ On ∧ 𝑥 ∈ On))
231		oacl 8573	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On) → (𝑥 +o 𝑥) ∈ On)
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (𝑥 +o 𝑥) ∈ On)
233		oecl 8575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
234	33, 232, 233	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
235	226, 234	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (𝑥 +o 𝑥)) ∈ On)
236	55	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ∈ On)
237		omwordri 8610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ On ∧ (ω ↑o (𝑥 +o 𝑥)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
238	223, 235, 236, 237	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶)))))
239	222, 238	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
240	226, 230, 231	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o 𝑥) ∈ On)
241	36	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ∈ On)
242		oeoa 8635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ω ∈ On ∧ (𝑥 +o 𝑥) ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
243	33, 240, 241, 242	mp3an2i 1468	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))))
244	226, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ On)
245		oaass 8599	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
246	244, 244, 241, 245	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o 𝐶))))
247		simpr1 1195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ (ω ↑o 𝐶))
248		ssidd 4007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
249		oaabs2 8687	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ↑o 𝐶) ∈ On) ∧ (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶)) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
250	247, 241, 248, 249	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
251	250	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (𝑥 +o (ω ↑o 𝐶))) = (𝑥 +o (ω ↑o 𝐶)))
252	246, 251, 250	3eqtrd 2781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
253	252	oveq2d 7447	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o ((𝑥 +o 𝑥) +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
254	243, 253	eqtr3d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (𝑥 +o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
255	239, 254	sseqtrd 4020	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (ω ↑o (ω ↑o 𝐶)))
256		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = (ω ↑o ∅))
257	256, 167	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = ∅ → (ω ↑o 𝑥) = 1o)
258	257	uneq2d 4168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ∪ 1o))
259	33	oneluni 6503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ∈ ω → (ω ∪ 1o) = ω)
260	63, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ω ∪ 1o) = ω
261	260, 163	eqtr4i 2768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ω ∪ 1o) = (ω ↑o 1o)
262	258, 261	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ∅ → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
263	262	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 1o))
264	263	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
265	224	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → 𝐶 ∈ On)
266		oecl 8575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((ω ∈ On ∧ ∅ ∈ On) → (ω ↑o ∅) ∈ On)
267	33, 73, 266	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ω ↑o ∅) ∈ On
268		oecl 8575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((ω ∈ On ∧ (ω ↑o ∅) ∈ On) → (ω ↑o (ω ↑o ∅)) ∈ On)
269	33, 267, 268	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ω ↑o (ω ↑o ∅)) ∈ On
270	269	2a1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ On))
271	270, 54	jca2 513	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On)))
272	167	oveq2i 7442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ω ↑o (ω ↑o ∅)) = (ω ↑o 1o)
273	272, 163	eqtri 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (ω ↑o (ω ↑o ∅)) = ω
274		ssun1 4178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ω ⊆ (ω ∪ (ω ↑o 𝑥))
275	273, 274	eqsstri 4030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ω ↑o (ω ↑o ∅)) ⊆ (ω ∪ (ω ↑o 𝑥))
276		simp2 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
277	275, 276	sstrid 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
278	277	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o ∅)) ⊆ 𝐴)
279	57	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ 𝐵)
280		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐵 = (ω ↑o (ω ↑o 𝐶)))
281	279, 280	eleqtrd 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ (ω ↑o (ω ↑o 𝐶)))
282	278, 281	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
283	282	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))))
284		ontr2 6431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ω ↑o (ω ↑o ∅)) ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω ↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω ↑o 𝐶))) → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
285	271, 283, 284	syl6ci 71	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
286		oeord 8626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∅ ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
287	73, 65, 286	mp3an13 1454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o ∅) ∈ (ω ↑o 𝐶)))
288	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐶 ∈ On → ω ∈ (On ∖ 2o))
289		oeord 8626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ω ↑o ∅) ∈ On ∧ (ω ↑o 𝐶) ∈ On ∧ ω ∈ (On ∖ 2o)) → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
290	267, 35, 288, 289	mp3an2i 1468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → ((ω ↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
291	287, 290	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 ↔ (ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶))))
292	291	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → ((ω ↑o (ω ↑o ∅)) ∈ (ω ↑o (ω ↑o 𝐶)) → ∅ ∈ 𝐶))
293	285, 292	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ∅ ∈ 𝐶))
294		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → Ord 𝐶)
295		ordsucss 7838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → suc ∅ ⊆ 𝐶))
296	94	sseq1i 4012	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶)
297	295, 296	imbitrrdi 252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝐶 → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
298	294, 297	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → (∅ ∈ 𝐶 → 1o ⊆ 𝐶))
299	293, 298	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → 1o ⊆ 𝐶))
300	265, 299	jcai 516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On ∧ 1o ⊆ 𝐶))
301	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → ω ∈ On)
302	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐶 ∈ On → 1o ∈ On)
303	301, 302, 35	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐶 ∈ On → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
304	303	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On))
305		oeoa 8635	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ω ∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
306	304, 305	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))))
307	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → 1o ∈ ω)
308	35	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 𝐶) ∈ On)
309		oeword 8628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
310	80, 65, 309	mp3an13 1454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐶 ∈ On → (1o ⊆ 𝐶 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝐶)))
311	310	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o 1o) ⊆ (ω ↑o 𝐶))
312	163, 311	eqsstrrid 4023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ω ⊆ (ω ↑o 𝐶))
313		oaabs 8686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1o ∈ ω ∧ (ω ↑o 𝐶) ∈ On) ∧ ω ⊆ (ω ↑o 𝐶)) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
314	307, 308, 312, 313	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
315	314	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → (ω ↑o (1o +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
316	306, 315	eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 1o ⊆ 𝐶) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
317	300, 316	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ↑o 1o) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
318	264, 317	eqtrd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
319	244, 195, 196	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (∅ ∈ 𝑥 → suc ∅ ⊆ 𝑥))
320	319	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → suc ∅ ⊆ 𝑥)
321	94, 320	eqsstrid 4022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 1o ⊆ 𝑥)
322	247	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ (ω ↑o 𝐶))
323	241, 322, 227	syl2an2r 685	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ On)
324	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ∈ (On ∖ 2o))
325		oeword 8628	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖ 2o)) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
326	80, 323, 324, 325	mp3an2i 1468	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (1o ⊆ 𝑥 ↔ (ω ↑o 1o) ⊆ (ω ↑o 𝑥)))
327	321, 326	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 1o) ⊆ (ω ↑o 𝑥))
328	163, 327	eqsstrrid 4023	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ⊆ (ω ↑o 𝑥))
329		ssequn1 4186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ω ⊆ (ω ↑o 𝑥) ↔ (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
330	328, 329	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ∪ (ω ↑o 𝑥)) = (ω ↑o 𝑥))
331	330	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
332	241	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ∈ On)
333		oeoa 8635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ 𝑥 ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
334	33, 323, 332, 333	mp3an2i 1468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω ↑o (ω ↑o 𝐶))))
335		ssidd 4007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o 𝐶) ⊆ (ω ↑o 𝐶))
336	322, 332, 335, 249	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (𝑥 +o (ω ↑o 𝐶)) = (ω ↑o 𝐶))
337	336	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ↑o (𝑥 +o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
338	331, 334, 337	3eqtr2d 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
339	226, 228, 201	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
340	318, 338, 339	mpjaodan 961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
341	276	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴)
342	33, 228, 75	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ↑o 𝑥) ∈ On)
343	342, 33	jctil 519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → (ω ∈ On ∧ (ω ↑o 𝑥) ∈ On))
344		onun2 6492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ω ∈ On ∧ (ω ↑o 𝑥) ∈ On) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
345	226, 343, 344	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪ (ω ↑o 𝑥)) ∈ On)
346		omwordri 8610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ω ∪ (ω ↑o 𝑥)) ∈ On ∧ 𝐴 ∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
347	345, 223, 236, 346	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶)))))
348	341, 347	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪ (ω ↑o 𝑥)) ·o (ω ↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
349	340, 348	eqsstrrd 4019	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ↑o (ω ↑o 𝐶)) ⊆ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))))
350	255, 349	eqssd 4001	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶)))
351	49	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω ↑o 𝐶))))
352	350, 351	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ (𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o 𝐵) = 𝐵)
353	352	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
354	353	ad5antr 734	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵))
355	141, 143, 221, 354	mp3and 1466	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
356	355	ex 412	. . . . . . . . . . . 12 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴 → (𝐴 ·o 𝐵) = 𝐵))
357	71, 356	syl5 34	. . . . . . . . . . 11 ⊢ (((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) ∧ 𝑧 ∈ (ω ↑o 𝑥)) → ((𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
358	357	rexlimdva 3155	. . . . . . . . . 10 ⊢ ((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖ 1o)) → (∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
359	358	rexlimdva 3155	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
360	359	rexlimdva 3155	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
361	360	exlimdv 1933	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
362	70, 361	syl5 34	. . . . . 6 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵))
363	69, 362	mpd 15	. . . . 5 ⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) ∧ ω ⊆ 𝐴) → (𝐴 ·o 𝐵) = 𝐵)
364		eloni 6394	. . . . . . 7 ⊢ (𝐴 ∈ On → Ord 𝐴)
365	59, 364	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → Ord 𝐴)
366		ordtri2or 6482	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord ω) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
367	365, 158, 366	sylancl 586	. . . . 5 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ∈ ω ∨ ω ⊆ 𝐴))
368	51, 363, 367	mpjaodan 961	. . . 4 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵)
369	368	ex 412	. . 3 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = 𝐵))
370	6, 30, 369	3jaod 1431	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On)) → (𝐴 ·o 𝐵) = 𝐵))
371	370	imp 406	1 ⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃!weu 2568   ≠ wne 2940  ∃wrex 3070   ∖ cdif 3948   ∪ cun 3949   ⊆ wss 3951  ∅c0 4333  {cpr 4628  ⟨cotp 4634  Ord word 6383  Oncon0 6384  suc csuc 6386  (class class class)co 7431  ωcom 7887  1_oc1o 8499  2_oc2o 8500   +_o coa 8503   ·_o comu 8504   ↑_o coe 8505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-reg 9632  ax-inf2 9681

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-omul 8511  df-oexp 8512

This theorem is referenced by:  omcl2  43346