omabs2

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

		Ref	Expression
	Assertion	omabs2	$⊢ ((A \in B \land \emptyset \in A) \land (B = \emptyset \lor B = 2_{𝑜} \lor (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On))) \to A \cdot_{𝑜} B = B$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ B = \emptyset \to (A \in B \leftrightarrow A \in \emptyset)$
2		noel	$⊢ \neg A \in \emptyset$
3	2	pm2.21i	$⊢ A \in \emptyset \to (\emptyset \in A \to A \cdot_{𝑜} B = B)$
4	1 3	biimtrdi	$⊢ B = \emptyset \to (A \in B \to (\emptyset \in A \to A \cdot_{𝑜} B = B))$
5	4	impd	$⊢ B = \emptyset \to ((A \in B \land \emptyset \in A) \to A \cdot_{𝑜} B = B)$
6	5	com12	$⊢ (A \in B \land \emptyset \in A) \to (B = \emptyset \to A \cdot_{𝑜} B = B)$
7		elpri	$⊢ A \in \{\emptyset, 1_{𝑜}\} \to (A = \emptyset \lor A = 1_{𝑜})$
8		eleq2	$⊢ A = \emptyset \to (\emptyset \in A \leftrightarrow \emptyset \in \emptyset)$
9		noel	$⊢ \neg \emptyset \in \emptyset$
10	9	pm2.21i	$⊢ \emptyset \in \emptyset \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜}$
11	8 10	biimtrdi	$⊢ A = \emptyset \to (\emptyset \in A \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
12		oveq1	$⊢ A = 1_{𝑜} \to A \cdot_{𝑜} 2_{𝑜} = 1_{𝑜} \cdot_{𝑜} 2_{𝑜}$
13		2on	$⊢ 2_{𝑜} \in On$
14		om1r	$⊢ 2_{𝑜} \in On \to 1_{𝑜} \cdot_{𝑜} 2_{𝑜} = 2_{𝑜}$
15	13 14	ax-mp	$⊢ 1_{𝑜} \cdot_{𝑜} 2_{𝑜} = 2_{𝑜}$
16	12 15	eqtrdi	$⊢ A = 1_{𝑜} \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜}$
17	16	a1d	$⊢ A = 1_{𝑜} \to (\emptyset \in A \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
18	11 17	jaoi	$⊢ (A = \emptyset \lor A = 1_{𝑜}) \to (\emptyset \in A \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
19	7 18	syl	$⊢ A \in \{\emptyset, 1_{𝑜}\} \to (\emptyset \in A \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
20		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
21	19 20	eleq2s	$⊢ A \in 2_{𝑜} \to (\emptyset \in A \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
22	21	imp	$⊢ (A \in 2_{𝑜} \land \emptyset \in A) \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜}$
23	22	a1i	$⊢ B = 2_{𝑜} \to ((A \in 2_{𝑜} \land \emptyset \in A) \to A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
24		eleq2	$⊢ B = 2_{𝑜} \to (A \in B \leftrightarrow A \in 2_{𝑜})$
25	24	anbi1d	$⊢ B = 2_{𝑜} \to ((A \in B \land \emptyset \in A) \leftrightarrow (A \in 2_{𝑜} \land \emptyset \in A))$
26		oveq2	$⊢ B = 2_{𝑜} \to A \cdot_{𝑜} B = A \cdot_{𝑜} 2_{𝑜}$
27		id	$⊢ B = 2_{𝑜} \to B = 2_{𝑜}$
28	26 27	eqeq12d	$⊢ B = 2_{𝑜} \to (A \cdot_{𝑜} B = B \leftrightarrow A \cdot_{𝑜} 2_{𝑜} = 2_{𝑜})$
29	23 25 28	3imtr4d	$⊢ B = 2_{𝑜} \to ((A \in B \land \emptyset \in A) \to A \cdot_{𝑜} B = B)$
30	29	com12	$⊢ (A \in B \land \emptyset \in A) \to (B = 2_{𝑜} \to A \cdot_{𝑜} B = B)$
31		simpr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to A \in ω$
32		simpllr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to \emptyset \in A$
33		omelon	$⊢ ω \in On$
34		oecl	$⊢ (ω \in On \land C \in On) \to ω ↑_{𝑜} C \in On$
35	33 34	mpan	$⊢ C \in On \to ω ↑_{𝑜} C \in On$
36	35	adantl	$⊢ (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to ω ↑_{𝑜} C \in On$
37	36	ad2antlr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to ω ↑_{𝑜} C \in On$
38	33	jctl	$⊢ C \in On \to (ω \in On \land C \in On)$
39		peano1	$⊢ \emptyset \in ω$
40		oen0	$⊢ ((ω \in On \land C \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} C)$
41	38 39 40	sylancl	$⊢ C \in On \to \emptyset \in (ω ↑_{𝑜} C)$
42	41	adantl	$⊢ (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to \emptyset \in (ω ↑_{𝑜} C)$
43	42	ad2antlr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to \emptyset \in (ω ↑_{𝑜} C)$
44		omabs	$⊢ ((A \in ω \land \emptyset \in A) \land (ω ↑_{𝑜} C \in On \land \emptyset \in (ω ↑_{𝑜} C))) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
45	31 32 37 43 44	syl22anc	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
46		oveq2	$⊢ B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \to A \cdot_{𝑜} B = A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
47		id	$⊢ B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \to B = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
48	46 47	eqeq12d	$⊢ B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \to (A \cdot_{𝑜} B = B \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C))$
49	48	adantr	$⊢ (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to (A \cdot_{𝑜} B = B \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C))$
50	49	ad2antlr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to (A \cdot_{𝑜} B = B \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C))$
51	45 50	mpbird	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land A \in ω) \to A \cdot_{𝑜} B = B$
52		simpl	$⊢ (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to B = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
53		oecl	$⊢ (ω \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On$
54	33 35 53	sylancr	$⊢ C \in On \to ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On$
55	54	adantl	$⊢ (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On$
56	52 55	eqeltrd	$⊢ (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to B \in On$
57		simpl	$⊢ (A \in B \land \emptyset \in A) \to A \in B$
58		onelon	$⊢ (B \in On \land A \in B) \to A \in On$
59	56 57 58	syl2anr	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to A \in On$
60		simplr	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to \emptyset \in A$
61		ondif1	$⊢ A \in (On ∖ 1_{𝑜}) \leftrightarrow (A \in On \land \emptyset \in A)$
62	59 60 61	sylanbrc	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to A \in (On ∖ 1_{𝑜})$
63		1onn	$⊢ 1_{𝑜} \in ω$
64		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
65	33 63 64	mpbir2an	$⊢ ω \in (On ∖ 2_{𝑜})$
66	62 65	jctil	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to (ω \in (On ∖ 2_{𝑜}) \land A \in (On ∖ 1_{𝑜}))$
67	66	adantr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to (ω \in (On ∖ 2_{𝑜}) \land A \in (On ∖ 1_{𝑜}))$
68		oeeu	$⊢ (ω \in (On ∖ 2_{𝑜}) \land A \in (On ∖ 1_{𝑜})) \to \exists! w \exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A)$
69	67 68	syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to \exists! w \exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A)$
70		euex	$⊢ \exists! w \exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to \exists w \exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A)$
71		simpr	$⊢ (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A$
72		0ss	$⊢ \emptyset \subseteq z$
73		0elon	$⊢ \emptyset \in On$
74		simpr	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \to x \in On$
75		oecl	$⊢ (ω \in On \land x \in On) \to ω ↑_{𝑜} x \in On$
76	33 74 75	sylancr	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \to ω ↑_{𝑜} x \in On$
77	76	ad2antrr	$⊢ ((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \to ω ↑_{𝑜} x \in On$
78		onelon	$⊢ (ω ↑_{𝑜} x \in On \land z \in (ω ↑_{𝑜} x)) \to z \in On$
79	77 78	sylancom	$⊢ ((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \to z \in On$
80		1on	$⊢ 1_{𝑜} \in On$
81		omcl	$⊢ (ω ↑_{𝑜} x \in On \land 1_{𝑜} \in On) \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On$
82	76 80 81	sylancl	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On$
83	82	ad3antrrr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On$
84		oaword	$⊢ (\emptyset \in On \land z \in On \land (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On) \to (\emptyset \subseteq z \leftrightarrow ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z)$
85	84	biimpd	$⊢ (\emptyset \in On \land z \in On \land (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On) \to (\emptyset \subseteq z \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z)$
86	73 79 83 85	mp3an2ani	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (\emptyset \subseteq z \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z)$
87	72 86	mpi	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z$
88		simpllr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to y \in (ω ∖ 1_{𝑜})$
89		omsson	$⊢ ω \subseteq On$
90		ssdif	$⊢ ω \subseteq On \to ω ∖ 1_{𝑜} \subseteq On ∖ 1_{𝑜}$
91	89 90	ax-mp	$⊢ ω ∖ 1_{𝑜} \subseteq On ∖ 1_{𝑜}$
92	91	sseli	$⊢ y \in (ω ∖ 1_{𝑜}) \to y \in (On ∖ 1_{𝑜})$
93		ondif1	$⊢ y \in (On ∖ 1_{𝑜}) \leftrightarrow (y \in On \land \emptyset \in y)$
94		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
95		eloni	$⊢ y \in On \to Ord y$
96		ordsucss	$⊢ Ord y \to (\emptyset \in y \to suc \emptyset \subseteq y)$
97	95 96	syl	$⊢ y \in On \to (\emptyset \in y \to suc \emptyset \subseteq y)$
98	97	imp	$⊢ (y \in On \land \emptyset \in y) \to suc \emptyset \subseteq y$
99	94 98	eqsstrid	$⊢ (y \in On \land \emptyset \in y) \to 1_{𝑜} \subseteq y$
100	93 99	sylbi	$⊢ y \in (On ∖ 1_{𝑜}) \to 1_{𝑜} \subseteq y$
101	88 92 100	3syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to 1_{𝑜} \subseteq y$
102		eldifi	$⊢ y \in (ω ∖ 1_{𝑜}) \to y \in ω$
103		nnon	$⊢ y \in ω \to y \in On$
104	102 103	syl	$⊢ y \in (ω ∖ 1_{𝑜}) \to y \in On$
105	104	ad2antlr	$⊢ ((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \to y \in On$
106		simp-4r	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to x \in On$
107	33 106 75	sylancr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} x \in On$
108		omwordi	$⊢ (1_{𝑜} \in On \land y \in On \land ω ↑_{𝑜} x \in On) \to (1_{𝑜} \subseteq y \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y)$
109	80 105 107 108	mp3an2ani	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (1_{𝑜} \subseteq y \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y)$
110	101 109	mpd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y$
111	105	adantr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to y \in On$
112		omcl	$⊢ (ω ↑_{𝑜} x \in On \land y \in On) \to (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On$
113	107 111 112	syl2anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On$
114	79	adantr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to z \in On$
115		oawordri	$⊢ ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On \land (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On \land z \in On) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z)$
116	83 113 114 115	syl3anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z)$
117	110 116	mpd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z$
118	87 117	sstrd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z$
119	33 75	mpan	$⊢ x \in On \to ω ↑_{𝑜} x \in On$
120	119 80 81	sylancl	$⊢ x \in On \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On$
121		oa0	$⊢ (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} \in On \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset = (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}$
122	120 121	syl	$⊢ x \in On \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset = (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}$
123		om1	$⊢ ω ↑_{𝑜} x \in On \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} = ω ↑_{𝑜} x$
124	119 123	syl	$⊢ x \in On \to (ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜} = ω ↑_{𝑜} x$
125	122 124	eqtrd	$⊢ x \in On \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset = ω ↑_{𝑜} x$
126	106 125	syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} \emptyset = ω ↑_{𝑜} x$
127		simpr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A$
128	118 126 127	3sstr3d	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} x \subseteq A$
129		simp-7l	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \in B$
130		simplrl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to B = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
131	130	ad4antr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to B = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
132	129 131	eleqtrd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
133	55	ad6antlr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On$
134		ontr2	$⊢ (ω ↑_{𝑜} x \in On \land ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On) \to ((ω ↑_{𝑜} x \subseteq A \land A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))) \to ω ↑_{𝑜} x \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
135	107 133 134	syl2anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x \subseteq A \land A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))) \to ω ↑_{𝑜} x \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
136	128 132 135	mp2and	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} x \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
137	36	ad6antlr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} C \in On$
138	65	a1i	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω \in (On ∖ 2_{𝑜})$
139		oeord	$⊢ (x \in On \land ω ↑_{𝑜} C \in On \land ω \in (On ∖ 2_{𝑜})) \to (x \in (ω ↑_{𝑜} C) \leftrightarrow ω ↑_{𝑜} x \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
140	106 137 138 139	syl3anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (x \in (ω ↑_{𝑜} C) \leftrightarrow ω ↑_{𝑜} x \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
141	136 140	mpbird	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to x \in (ω ↑_{𝑜} C)$
142		simp-5r	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω \subseteq A$
143	142 128	unssd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω \cup (ω ↑_{𝑜} x) \subseteq A$
144		simplr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to z \in (ω ↑_{𝑜} x)$
145		onelpss	$⊢ (z \in On \land ω ↑_{𝑜} x \in On) \to (z \in (ω ↑_{𝑜} x) \leftrightarrow (z \subseteq ω ↑_{𝑜} x \land z \neq ω ↑_{𝑜} x))$
146	145	biimpd	$⊢ (z \in On \land ω ↑_{𝑜} x \in On) \to (z \in (ω ↑_{𝑜} x) \to (z \subseteq ω ↑_{𝑜} x \land z \neq ω ↑_{𝑜} x))$
147	79 107 146	syl2an2r	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (z \in (ω ↑_{𝑜} x) \to (z \subseteq ω ↑_{𝑜} x \land z \neq ω ↑_{𝑜} x))$
148	144 147	mpd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (z \subseteq ω ↑_{𝑜} x \land z \neq ω ↑_{𝑜} x)$
149		simpl	$⊢ (z \subseteq ω ↑_{𝑜} x \land z \neq ω ↑_{𝑜} x) \to z \subseteq ω ↑_{𝑜} x$
150	148 149	syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to z \subseteq ω ↑_{𝑜} x$
151		oaword	$⊢ (z \in On \land ω ↑_{𝑜} x \in On \land (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On) \to (z \subseteq ω ↑_{𝑜} x \leftrightarrow ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} x))$
152	151	biimpd	$⊢ (z \in On \land ω ↑_{𝑜} x \in On \land (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On) \to (z \subseteq ω ↑_{𝑜} x \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} x))$
153	114 107 113 152	syl3anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (z \subseteq ω ↑_{𝑜} x \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} x))$
154	150 153	mpd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} x)$
155		omsuc	$⊢ (ω ↑_{𝑜} x \in On \land y \in On) \to (ω ↑_{𝑜} x) \cdot_{𝑜} suc y = ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} x)$
156	107 111 155	syl2anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (ω ↑_{𝑜} x) \cdot_{𝑜} suc y = ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} x)$
157	154 156	sseqtrrd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} suc y$
158		ordom	$⊢ Ord ω$
159	88 102	syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to y \in ω$
160		ordsucss	$⊢ Ord ω \to (y \in ω \to suc y \subseteq ω)$
161	158 159 160	mpsyl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to suc y \subseteq ω$
162		oe1	$⊢ ω \in On \to ω ↑_{𝑜} 1_{𝑜} = ω$
163	33 162	ax-mp	$⊢ ω ↑_{𝑜} 1_{𝑜} = ω$
164		simpr	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to x = \emptyset$
165	164	oveq2d	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to ω ↑_{𝑜} x = ω ↑_{𝑜} \emptyset$
166		oe0	$⊢ ω \in On \to ω ↑_{𝑜} \emptyset = 1_{𝑜}$
167	33 166	ax-mp	$⊢ ω ↑_{𝑜} \emptyset = 1_{𝑜}$
168	165 167	eqtrdi	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to ω ↑_{𝑜} x = 1_{𝑜}$
169	168	oveq1d	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to (ω ↑_{𝑜} x) \cdot_{𝑜} y = 1_{𝑜} \cdot_{𝑜} y$
170	104	adantl	$⊢ (((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \to y \in On$
171	170	ad3antrrr	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to y \in On$
172		om1r	$⊢ y \in On \to 1_{𝑜} \cdot_{𝑜} y = y$
173	171 172	syl	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to 1_{𝑜} \cdot_{𝑜} y = y$
174	169 173	eqtrd	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to (ω ↑_{𝑜} x) \cdot_{𝑜} y = y$
175		simpllr	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to z \in (ω ↑_{𝑜} x)$
176	175 168	eleqtrd	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to z \in 1_{𝑜}$
177		el1o	$⊢ z \in 1_{𝑜} \leftrightarrow z = \emptyset$
178	176 177	sylib	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to z = \emptyset$
179	174 178	oveq12d	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = y +_{𝑜} \emptyset$
180		simplr	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A$
181		oa0	$⊢ y \in On \to y +_{𝑜} \emptyset = y$
182	171 181	syl	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to y +_{𝑜} \emptyset = y$
183	179 180 182	3eqtr3d	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to A = y$
184	159	adantr	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to y \in ω$
185	183 184	eqeltrd	$⊢ ((((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \land x = \emptyset) \to A \in ω$
186	185	ex	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (x = \emptyset \to A \in ω)$
187	33 33	pm3.2i	$⊢ (ω \in On \land ω \in On)$
188		ontr2	$⊢ (ω \in On \land ω \in On) \to ((ω \subseteq A \land A \in ω) \to ω \in ω)$
189	188	expd	$⊢ (ω \in On \land ω \in On) \to (ω \subseteq A \to (A \in ω \to ω \in ω))$
190	187 142 189	mpsyl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (A \in ω \to ω \in ω)$
191		elirr	$⊢ \neg ω \in ω$
192	191	pm2.21i	$⊢ ω \in ω \to 1_{𝑜} \subseteq x$
193	192	a1i	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (ω \in ω \to 1_{𝑜} \subseteq x)$
194	186 190 193	3syld	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (x = \emptyset \to 1_{𝑜} \subseteq x)$
195		eloni	$⊢ x \in On \to Ord x$
196		ordsucss	$⊢ Ord x \to (\emptyset \in x \to suc \emptyset \subseteq x)$
197	196	imp	$⊢ (Ord x \land \emptyset \in x) \to suc \emptyset \subseteq x$
198	94 197	eqsstrid	$⊢ (Ord x \land \emptyset \in x) \to 1_{𝑜} \subseteq x$
199	198	ex	$⊢ Ord x \to (\emptyset \in x \to 1_{𝑜} \subseteq x)$
200	106 195 199	3syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (\emptyset \in x \to 1_{𝑜} \subseteq x)$
201		on0eqel	$⊢ x \in On \to (x = \emptyset \lor \emptyset \in x)$
202	106 201	syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (x = \emptyset \lor \emptyset \in x)$
203	194 200 202	mpjaod	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to 1_{𝑜} \subseteq x$
204	80	a1i	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to 1_{𝑜} \in On$
205	33	a1i	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω \in On$
206	204 106 205	3jca	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (1_{𝑜} \in On \land x \in On \land ω \in On)$
207		oewordi	$⊢ ((1_{𝑜} \in On \land x \in On \land ω \in On) \land \emptyset \in ω) \to (1_{𝑜} \subseteq x \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x)$
208	206 39 207	sylancl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (1_{𝑜} \subseteq x \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x)$
209	203 208	mpd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x$
210	163 209	eqsstrrid	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω \subseteq ω ↑_{𝑜} x$
211	161 210	sstrd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to suc y \subseteq ω ↑_{𝑜} x$
212		onsuc	$⊢ y \in On \to suc y \in On$
213	111 212	syl	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to suc y \in On$
214		omwordi	$⊢ (suc y \in On \land ω ↑_{𝑜} x \in On \land ω ↑_{𝑜} x \in On) \to (suc y \subseteq ω ↑_{𝑜} x \to (ω ↑_{𝑜} x) \cdot_{𝑜} suc y \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x))$
215	213 107 107 214	syl3anc	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (suc y \subseteq ω ↑_{𝑜} x \to (ω ↑_{𝑜} x) \cdot_{𝑜} suc y \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x))$
216	211 215	mpd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to (ω ↑_{𝑜} x) \cdot_{𝑜} suc y \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x)$
217	157 216	sstrd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x)$
218	127	eqcomd	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A = ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z$
219		oeoa	$⊢ (ω \in On \land x \in On \land x \in On) \to ω ↑_{𝑜} (x +_{𝑜} x) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x)$
220	33 106 106 219	mp3an2i	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ω ↑_{𝑜} (x +_{𝑜} x) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x)$
221	217 218 220	3sstr4d	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)$
222		simpr3	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)$
223	59	adantr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \in On$
224		simprr	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to C \in On$
225		simp1	$⊢ (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to x \in (ω ↑_{𝑜} C)$
226	224 225	anim12i	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (C \in On \land x \in (ω ↑_{𝑜} C))$
227		onelon	$⊢ (ω ↑_{𝑜} C \in On \land x \in (ω ↑_{𝑜} C)) \to x \in On$
228	35 227	sylan	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to x \in On$
229		pm4.24	$⊢ x \in On \leftrightarrow (x \in On \land x \in On)$
230	228 229	sylib	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to (x \in On \land x \in On)$
231		oacl	$⊢ (x \in On \land x \in On) \to x +_{𝑜} x \in On$
232	230 231	syl	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to x +_{𝑜} x \in On$
233		oecl	$⊢ (ω \in On \land x +_{𝑜} x \in On) \to ω ↑_{𝑜} (x +_{𝑜} x) \in On$
234	33 232 233	sylancr	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to ω ↑_{𝑜} (x +_{𝑜} x) \in On$
235	226 234	syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} (x +_{𝑜} x) \in On$
236	55	ad2antlr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On$
237		omwordri	$⊢ (A \in On \land ω ↑_{𝑜} (x +_{𝑜} x) \in On \land ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On) \to (A \subseteq ω ↑_{𝑜} (x +_{𝑜} x) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
238	223 235 236 237	syl3anc	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (A \subseteq ω ↑_{𝑜} (x +_{𝑜} x) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
239	222 238	mpd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
240	226 230 231	3syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to x +_{𝑜} x \in On$
241	36	ad2antlr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} C \in On$
242		oeoa	$⊢ (ω \in On \land x +_{𝑜} x \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} ((x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
243	33 240 241 242	mp3an2i	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} ((x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
244	226 228	syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to x \in On$
245		oaass	$⊢ (x \in On \land x \in On \land ω ↑_{𝑜} C \in On) \to (x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C) = x +_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C))$
246	244 244 241 245	syl3anc	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C) = x +_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C))$
247		simpr1	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to x \in (ω ↑_{𝑜} C)$
248		ssidd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} C \subseteq ω ↑_{𝑜} C$
249		oaabs2	$⊢ ((x \in (ω ↑_{𝑜} C) \land ω ↑_{𝑜} C \in On) \land ω ↑_{𝑜} C \subseteq ω ↑_{𝑜} C) \to x +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
250	247 241 248 249	syl21anc	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to x +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
251	250	oveq2d	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to x +_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C)) = x +_{𝑜} (ω ↑_{𝑜} C)$
252	246 251 250	3eqtrd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
253	252	oveq2d	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} ((x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
254	243 253	eqtr3d	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
255	239 254	sseqtrd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq ω ↑_{𝑜} (ω ↑_{𝑜} C)$
256		oveq2	$⊢ x = \emptyset \to ω ↑_{𝑜} x = ω ↑_{𝑜} \emptyset$
257	256 167	eqtrdi	$⊢ x = \emptyset \to ω ↑_{𝑜} x = 1_{𝑜}$
258	257	uneq2d	$⊢ x = \emptyset \to ω \cup (ω ↑_{𝑜} x) = ω \cup 1_{𝑜}$
259	33	oneluni	$⊢ 1_{𝑜} \in ω \to ω \cup 1_{𝑜} = ω$
260	63 259	ax-mp	$⊢ ω \cup 1_{𝑜} = ω$
261	260 163	eqtr4i	$⊢ ω \cup 1_{𝑜} = ω ↑_{𝑜} 1_{𝑜}$
262	258 261	eqtrdi	$⊢ x = \emptyset \to ω \cup (ω ↑_{𝑜} x) = ω ↑_{𝑜} 1_{𝑜}$
263	262	adantl	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to ω \cup (ω ↑_{𝑜} x) = ω ↑_{𝑜} 1_{𝑜}$
264	263	oveq1d	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
265	224	ad2antrr	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to C \in On$
266		oecl	$⊢ (ω \in On \land \emptyset \in On) \to ω ↑_{𝑜} \emptyset \in On$
267	33 73 266	mp2an	$⊢ ω ↑_{𝑜} \emptyset \in On$
268		oecl	$⊢ (ω \in On \land ω ↑_{𝑜} \emptyset \in On) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On$
269	33 267 268	mp2an	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On$
270	269	2a1i	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (C \in On \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On)$
271	270 54	jca2	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (C \in On \to (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On \land ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On))$
272	167	oveq2i	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) = ω ↑_{𝑜} 1_{𝑜}$
273	272 163	eqtri	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) = ω$
274		ssun1	$⊢ ω \subseteq ω \cup (ω ↑_{𝑜} x)$
275	273 274	eqsstri	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq ω \cup (ω ↑_{𝑜} x)$
276		simp2	$⊢ (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to ω \cup (ω ↑_{𝑜} x) \subseteq A$
277	275 276	sstrid	$⊢ (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A$
278	277	adantl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A$
279	57	ad2antrr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \in B$
280		simplrl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to B = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
281	279 280	eleqtrd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
282	278 281	jca	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A \land A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
283	282	adantr	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A \land A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
284		ontr2	$⊢ (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On \land ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On) \to ((ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A \land A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
285	271 283 284	syl6ci	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (C \in On \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
286		oeord	$⊢ (\emptyset \in On \land C \in On \land ω \in (On ∖ 2_{𝑜})) \to (\emptyset \in C \leftrightarrow ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C))$
287	73 65 286	mp3an13	$⊢ C \in On \to (\emptyset \in C \leftrightarrow ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C))$
288	65	a1i	$⊢ C \in On \to ω \in (On ∖ 2_{𝑜})$
289		oeord	$⊢ (ω ↑_{𝑜} \emptyset \in On \land ω ↑_{𝑜} C \in On \land ω \in (On ∖ 2_{𝑜})) \to (ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C) \leftrightarrow ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
290	267 35 288 289	mp3an2i	$⊢ C \in On \to (ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C) \leftrightarrow ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
291	287 290	bitrd	$⊢ C \in On \to (\emptyset \in C \leftrightarrow ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
292	291	biimprd	$⊢ C \in On \to (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \to \emptyset \in C)$
293	285 292	sylcom	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (C \in On \to \emptyset \in C)$
294		eloni	$⊢ C \in On \to Ord C$
295		ordsucss	$⊢ Ord C \to (\emptyset \in C \to suc \emptyset \subseteq C)$
296	94	sseq1i	$⊢ 1_{𝑜} \subseteq C \leftrightarrow suc \emptyset \subseteq C$
297	295 296	imbitrrdi	$⊢ Ord C \to (\emptyset \in C \to 1_{𝑜} \subseteq C)$
298	294 297	syl	$⊢ C \in On \to (\emptyset \in C \to 1_{𝑜} \subseteq C)$
299	293 298	sylcom	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (C \in On \to 1_{𝑜} \subseteq C)$
300	265 299	jcai	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (C \in On \land 1_{𝑜} \subseteq C)$
301	33	a1i	$⊢ C \in On \to ω \in On$
302	80	a1i	$⊢ C \in On \to 1_{𝑜} \in On$
303	301 302 35	3jca	$⊢ C \in On \to (ω \in On \land 1_{𝑜} \in On \land ω ↑_{𝑜} C \in On)$
304	303	adantr	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to (ω \in On \land 1_{𝑜} \in On \land ω ↑_{𝑜} C \in On)$
305		oeoa	$⊢ (ω \in On \land 1_{𝑜} \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} (1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
306	304 305	syl	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} (1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
307	63	a1i	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to 1_{𝑜} \in ω$
308	35	adantr	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} C \in On$
309		oeword	$⊢ (1_{𝑜} \in On \land C \in On \land ω \in (On ∖ 2_{𝑜})) \to (1_{𝑜} \subseteq C \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} C)$
310	80 65 309	mp3an13	$⊢ C \in On \to (1_{𝑜} \subseteq C \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} C)$
311	310	biimpa	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} C$
312	163 311	eqsstrrid	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω \subseteq ω ↑_{𝑜} C$
313		oaabs	$⊢ ((1_{𝑜} \in ω \land ω ↑_{𝑜} C \in On) \land ω \subseteq ω ↑_{𝑜} C) \to 1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
314	307 308 312 313	syl21anc	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to 1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
315	314	oveq2d	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} (1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
316	306 315	eqtr3d	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
317	300 316	syl	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
318	264 317	eqtrd	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land x = \emptyset) \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
319	244 195 196	3syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (\emptyset \in x \to suc \emptyset \subseteq x)$
320	319	imp	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to suc \emptyset \subseteq x$
321	94 320	eqsstrid	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to 1_{𝑜} \subseteq x$
322	247	adantr	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to x \in (ω ↑_{𝑜} C)$
323	241 322 227	syl2an2r	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to x \in On$
324	65	a1i	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω \in (On ∖ 2_{𝑜})$
325		oeword	$⊢ (1_{𝑜} \in On \land x \in On \land ω \in (On ∖ 2_{𝑜})) \to (1_{𝑜} \subseteq x \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x)$
326	80 323 324 325	mp3an2i	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to (1_{𝑜} \subseteq x \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x)$
327	321 326	mpbid	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x$
328	163 327	eqsstrrid	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω \subseteq ω ↑_{𝑜} x$
329		ssequn1	$⊢ ω \subseteq ω ↑_{𝑜} x \leftrightarrow ω \cup (ω ↑_{𝑜} x) = ω ↑_{𝑜} x$
330	328 329	sylib	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω \cup (ω ↑_{𝑜} x) = ω ↑_{𝑜} x$
331	330	oveq1d	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
332	241	adantr	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω ↑_{𝑜} C \in On$
333		oeoa	$⊢ (ω \in On \land x \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
334	33 323 332 333	mp3an2i	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω ↑_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
335		ssidd	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω ↑_{𝑜} C \subseteq ω ↑_{𝑜} C$
336	322 332 335 249	syl21anc	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to x +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
337	336	oveq2d	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to ω ↑_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
338	331 334 337	3eqtr2d	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \land \emptyset \in x) \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
339	226 228 201	3syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (x = \emptyset \lor \emptyset \in x)$
340	318 338 339	mpjaodan	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
341	276	adantl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω \cup (ω ↑_{𝑜} x) \subseteq A$
342	33 228 75	sylancr	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to ω ↑_{𝑜} x \in On$
343	342 33	jctil	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to (ω \in On \land ω ↑_{𝑜} x \in On)$
344		onun2	$⊢ (ω \in On \land ω ↑_{𝑜} x \in On) \to ω \cup (ω ↑_{𝑜} x) \in On$
345	226 343 344	3syl	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω \cup (ω ↑_{𝑜} x) \in On$
346		omwordri	$⊢ (ω \cup (ω ↑_{𝑜} x) \in On \land A \in On \land ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On) \to (ω \cup (ω ↑_{𝑜} x) \subseteq A \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
347	345 223 236 346	syl3anc	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (ω \cup (ω ↑_{𝑜} x) \subseteq A \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
348	341 347	mpd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (ω \cup (ω ↑_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \subseteq A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
349	340 348	eqsstrrd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to ω ↑_{𝑜} (ω ↑_{𝑜} C) \subseteq A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
350	255 349	eqssd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
351	49	ad2antlr	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to (A \cdot_{𝑜} B = B \leftrightarrow A \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C))$
352	350 351	mpbird	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x))) \to A \cdot_{𝑜} B = B$
353	352	ex	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to ((x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to A \cdot_{𝑜} B = B)$
354	353	ad5antr	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to ((x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to A \cdot_{𝑜} B = B)$
355	141 143 221 354	mp3and	$⊢ (((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B$
356	355	ex	$⊢ ((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \to (((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A \to A \cdot_{𝑜} B = B)$
357	71 356	syl5	$⊢ ((((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \land z \in (ω ↑_{𝑜} x)) \to ((w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B)$
358	357	rexlimdva	$⊢ (((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \land y \in (ω ∖ 1_{𝑜})) \to (\exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B)$
359	358	rexlimdva	$⊢ ((((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \land x \in On) \to (\exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B)$
360	359	rexlimdva	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to (\exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B)$
361	360	exlimdv	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to (\exists w \exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B)$
362	70 361	syl5	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to (\exists! w \exists x \in On \exists y \in (ω ∖ 1_{𝑜}) \exists z \in (ω ↑_{𝑜} x) (w = ⟨x, y, z⟩ \land ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} z = A) \to A \cdot_{𝑜} B = B)$
363	69 362	mpd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to A \cdot_{𝑜} B = B$
364		eloni	$⊢ A \in On \to Ord A$
365	59 364	syl	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to Ord A$
366		ordtri2or	$⊢ (Ord A \land Ord ω) \to (A \in ω \lor ω \subseteq A)$
367	365 158 366	sylancl	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to (A \in ω \lor ω \subseteq A)$
368	51 363 367	mpjaodan	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to A \cdot_{𝑜} B = B$
369	368	ex	$⊢ (A \in B \land \emptyset \in A) \to ((B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to A \cdot_{𝑜} B = B)$
370	6 30 369	3jaod	$⊢ (A \in B \land \emptyset \in A) \to ((B = \emptyset \lor B = 2_{𝑜} \lor (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to A \cdot_{𝑜} B = B)$
371	370	imp	$⊢ ((A \in B \land \emptyset \in A) \land (B = \emptyset \lor B = 2_{𝑜} \lor (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On))) \to A \cdot_{𝑜} B = B$

Metamath Proof Explorer

Theorem omabs2

Proof