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		ordirr	$⊢ Ord ω \to \neg ω \in ω$
192	158 191	ax-mp	$⊢ \neg ω \in ω$
193	192	pm2.21i	$⊢ ω \in ω \to 1_{𝑜} \subseteq x$
194	193	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)$
195	186 190 194	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)$
196		eloni	$⊢ x \in On \to Ord x$
197		ordsucss	$⊢ Ord x \to (\emptyset \in x \to suc \emptyset \subseteq x)$
198	197	imp	$⊢ (Ord x \land \emptyset \in x) \to suc \emptyset \subseteq x$
199	94 198	eqsstrid	$⊢ (Ord x \land \emptyset \in x) \to 1_{𝑜} \subseteq x$
200	199	ex	$⊢ Ord x \to (\emptyset \in x \to 1_{𝑜} \subseteq x)$
201	106 196 200	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)$
202		on0eqel	$⊢ x \in On \to (x = \emptyset \lor \emptyset \in x)$
203	106 202	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)$
204	195 201 203	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$
205	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$
206	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$
207	205 106 206	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)$
208		oewordi	$⊢ ((1_{𝑜} \in On \land x \in On \land ω \in On) \land \emptyset \in ω) \to (1_{𝑜} \subseteq x \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x)$
209	207 39 208	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)$
210	204 209	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$
211	163 210	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$
212	161 211	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$
213		onsuc	$⊢ y \in On \to suc y \in On$
214	111 213	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$
215		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))$
216	214 107 107 215	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))$
217	212 216	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)$
218	157 217	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)$
219	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$
220		oeoa	$⊢ (ω \in On \land x \in On \land x \in On) \to ω ↑_{𝑜} (x +_{𝑜} x) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} x)$
221	33 106 106 220	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)$
222	218 219 221	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)$
223		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)$
224	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$
225		simprr	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to C \in On$
226		simp1	$⊢ (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to x \in (ω ↑_{𝑜} C)$
227	225 226	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))$
228		onelon	$⊢ (ω ↑_{𝑜} C \in On \land x \in (ω ↑_{𝑜} C)) \to x \in On$
229	35 228	sylan	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to x \in On$
230		pm4.24	$⊢ x \in On \leftrightarrow (x \in On \land x \in On)$
231	229 230	sylib	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to (x \in On \land x \in On)$
232		oacl	$⊢ (x \in On \land x \in On) \to x +_{𝑜} x \in On$
233	231 232	syl	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to x +_{𝑜} x \in On$
234		oecl	$⊢ (ω \in On \land x +_{𝑜} x \in On) \to ω ↑_{𝑜} (x +_{𝑜} x) \in On$
235	33 233 234	sylancr	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to ω ↑_{𝑜} (x +_{𝑜} x) \in On$
236	227 235	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$
237	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$
238		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)))$
239	224 236 237 238	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)))$
240	223 239	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))$
241	227 231 232	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$
242	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$
243		oeoa	$⊢ (ω \in On \land x +_{𝑜} x \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} ((x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} (x +_{𝑜} x)) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
244	33 241 242 243	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))$
245	227 229	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$
246		oaass	$⊢ (x \in On \land x \in On \land ω ↑_{𝑜} C \in On) \to (x +_{𝑜} x) +_{𝑜} (ω ↑_{𝑜} C) = x +_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C))$
247	245 245 242 246	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))$
248		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)$
249		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$
250		oaabs2	$⊢ ((x \in (ω ↑_{𝑜} C) \land ω ↑_{𝑜} C \in On) \land ω ↑_{𝑜} C \subseteq ω ↑_{𝑜} C) \to x +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
251	248 242 249 250	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$
252	251	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)$
253	247 252 251	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$
254	253	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)$
255	244 254	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)$
256	240 255	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)$
257		oveq2	$⊢ x = \emptyset \to ω ↑_{𝑜} x = ω ↑_{𝑜} \emptyset$
258	257 167	eqtrdi	$⊢ x = \emptyset \to ω ↑_{𝑜} x = 1_{𝑜}$
259	258	uneq2d	$⊢ x = \emptyset \to ω \cup (ω ↑_{𝑜} x) = ω \cup 1_{𝑜}$
260	33	oneluni	$⊢ 1_{𝑜} \in ω \to ω \cup 1_{𝑜} = ω$
261	63 260	ax-mp	$⊢ ω \cup 1_{𝑜} = ω$
262	261 163	eqtr4i	$⊢ ω \cup 1_{𝑜} = ω ↑_{𝑜} 1_{𝑜}$
263	259 262	eqtrdi	$⊢ x = \emptyset \to ω \cup (ω ↑_{𝑜} x) = ω ↑_{𝑜} 1_{𝑜}$
264	263	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_{𝑜}$
265	264	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))$
266	225	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$
267		oecl	$⊢ (ω \in On \land \emptyset \in On) \to ω ↑_{𝑜} \emptyset \in On$
268	33 73 267	mp2an	$⊢ ω ↑_{𝑜} \emptyset \in On$
269		oecl	$⊢ (ω \in On \land ω ↑_{𝑜} \emptyset \in On) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On$
270	33 268 269	mp2an	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On$
271	270	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)$
272	271 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))$
273	167	oveq2i	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) = ω ↑_{𝑜} 1_{𝑜}$
274	273 163	eqtri	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) = ω$
275		ssun1	$⊢ ω \subseteq ω \cup (ω ↑_{𝑜} x)$
276	274 275	eqsstri	$⊢ ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq ω \cup (ω ↑_{𝑜} x)$
277		simp2	$⊢ (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to ω \cup (ω ↑_{𝑜} x) \subseteq A$
278	276 277	sstrid	$⊢ (x \in (ω ↑_{𝑜} C) \land ω \cup (ω ↑_{𝑜} x) \subseteq A \land A \subseteq ω ↑_{𝑜} (x +_{𝑜} x)) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A$
279	278	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$
280	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$
281		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)$
282	280 281	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))$
283	279 282	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)))$
284	283	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)))$
285		ontr2	$⊢ (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in On \land ω ↑_{𝑜} (ω ↑_{𝑜} C) \in On) \to ((ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \subseteq A \land A \in (ω ↑_{𝑜} (ω ↑_{𝑜} C))) \to ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
286	272 284 285	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)))$
287		oeord	$⊢ (\emptyset \in On \land C \in On \land ω \in (On ∖ 2_{𝑜})) \to (\emptyset \in C \leftrightarrow ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C))$
288	73 65 287	mp3an13	$⊢ C \in On \to (\emptyset \in C \leftrightarrow ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C))$
289	65	a1i	$⊢ C \in On \to ω \in (On ∖ 2_{𝑜})$
290		oeord	$⊢ (ω ↑_{𝑜} \emptyset \in On \land ω ↑_{𝑜} C \in On \land ω \in (On ∖ 2_{𝑜})) \to (ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C) \leftrightarrow ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
291	268 35 289 290	mp3an2i	$⊢ C \in On \to (ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} C) \leftrightarrow ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
292	288 291	bitrd	$⊢ C \in On \to (\emptyset \in C \leftrightarrow ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)))$
293	292	biimprd	$⊢ C \in On \to (ω ↑_{𝑜} (ω ↑_{𝑜} \emptyset) \in (ω ↑_{𝑜} (ω ↑_{𝑜} C)) \to \emptyset \in C)$
294	286 293	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)$
295		eloni	$⊢ C \in On \to Ord C$
296		ordsucss	$⊢ Ord C \to (\emptyset \in C \to suc \emptyset \subseteq C)$
297	94	sseq1i	$⊢ 1_{𝑜} \subseteq C \leftrightarrow suc \emptyset \subseteq C$
298	296 297	imbitrrdi	$⊢ Ord C \to (\emptyset \in C \to 1_{𝑜} \subseteq C)$
299	295 298	syl	$⊢ C \in On \to (\emptyset \in C \to 1_{𝑜} \subseteq C)$
300	294 299	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)$
301	266 300	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)$
302	33	a1i	$⊢ C \in On \to ω \in On$
303	80	a1i	$⊢ C \in On \to 1_{𝑜} \in On$
304	302 303 35	3jca	$⊢ C \in On \to (ω \in On \land 1_{𝑜} \in On \land ω ↑_{𝑜} C \in On)$
305	304	adantr	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to (ω \in On \land 1_{𝑜} \in On \land ω ↑_{𝑜} C \in On)$
306		oeoa	$⊢ (ω \in On \land 1_{𝑜} \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} (1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
307	305 306	syl	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} (1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
308	63	a1i	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to 1_{𝑜} \in ω$
309	35	adantr	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} C \in On$
310		oeword	$⊢ (1_{𝑜} \in On \land C \in On \land ω \in (On ∖ 2_{𝑜})) \to (1_{𝑜} \subseteq C \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} C)$
311	80 65 310	mp3an13	$⊢ C \in On \to (1_{𝑜} \subseteq C \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} C)$
312	311	biimpa	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} C$
313	163 312	eqsstrrid	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω \subseteq ω ↑_{𝑜} C$
314		oaabs	$⊢ ((1_{𝑜} \in ω \land ω ↑_{𝑜} C \in On) \land ω \subseteq ω ↑_{𝑜} C) \to 1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
315	308 309 313 314	syl21anc	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to 1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
316	315	oveq2d	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to ω ↑_{𝑜} (1_{𝑜} +_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
317	307 316	eqtr3d	$⊢ (C \in On \land 1_{𝑜} \subseteq C) \to (ω ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C)) = ω ↑_{𝑜} (ω ↑_{𝑜} C)$
318	301 317	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)$
319	265 318	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)$
320	245 196 197	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)$
321	320	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$
322	94 321	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$
323	248	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)$
324	242 323 228	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$
325	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_{𝑜})$
326		oeword	$⊢ (1_{𝑜} \in On \land x \in On \land ω \in (On ∖ 2_{𝑜})) \to (1_{𝑜} \subseteq x \leftrightarrow ω ↑_{𝑜} 1_{𝑜} \subseteq ω ↑_{𝑜} x)$
327	80 324 325 326	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)$
328	322 327	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$
329	163 328	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$
330		ssequn1	$⊢ ω \subseteq ω ↑_{𝑜} x \leftrightarrow ω \cup (ω ↑_{𝑜} x) = ω ↑_{𝑜} x$
331	329 330	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$
332	331	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))$
333	242	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$
334		oeoa	$⊢ (ω \in On \land x \in On \land ω ↑_{𝑜} C \in On) \to ω ↑_{𝑜} (x +_{𝑜} (ω ↑_{𝑜} C)) = (ω ↑_{𝑜} x) \cdot_{𝑜} (ω ↑_{𝑜} (ω ↑_{𝑜} C))$
335	33 324 333 334	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))$
336		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$
337	323 333 336 250	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$
338	337	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)$
339	332 335 338	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)$
340	227 229 202	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)$
341	319 339 340	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)$
342	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 ω \cup (ω ↑_{𝑜} x) \subseteq A$
343	33 229 75	sylancr	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to ω ↑_{𝑜} x \in On$
344	343 33	jctil	$⊢ (C \in On \land x \in (ω ↑_{𝑜} C)) \to (ω \in On \land ω ↑_{𝑜} x \in On)$
345		onun2	$⊢ (ω \in On \land ω ↑_{𝑜} x \in On) \to ω \cup (ω ↑_{𝑜} x) \in On$
346	227 344 345	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$
347		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)))$
348	346 224 237 347	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)))$
349	342 348	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))$
350	341 349	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))$
351	256 350	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)$
352	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))$
353	351 352	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$
354	353	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)$
355	354	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)$
356	141 143 222 355	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$
357	356	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)$
358	71 357	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)$
359	358	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)$
360	359	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)$
361	360	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)$
362	361	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)$
363	70 362	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)$
364	69 363	mpd	$⊢ (((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \land ω \subseteq A) \to A \cdot_{𝑜} B = B$
365		eloni	$⊢ A \in On \to Ord A$
366	59 365	syl	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to Ord A$
367		ordtri2or	$⊢ (Ord A \land Ord ω) \to (A \in ω \lor ω \subseteq A)$
368	366 158 367	sylancl	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to (A \in ω \lor ω \subseteq A)$
369	51 364 368	mpjaodan	$⊢ ((A \in B \land \emptyset \in A) \land (B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On)) \to A \cdot_{𝑜} B = B$
370	369	ex	$⊢ (A \in B \land \emptyset \in A) \to ((B = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On) \to A \cdot_{𝑜} B = B)$
371	6 30 370	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)$
372	371	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