oaabs2

Description: The absorption law oaabs is also a property of higher powers of _om . (Contributed by Mario Carneiro, 29-May-2015)

		Ref	Expression
	Assertion	oaabs2	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to A +_{𝑜} B = B$

Proof

Step	Hyp	Ref	Expression
1		n0i	$⊢ A \in (ω ↑_{𝑜} C) \to \neg ω ↑_{𝑜} C = \emptyset$
2		fnoe	$⊢ ↑_{𝑜} Fn (On \times On)$
3		fndm	$⊢ ↑_{𝑜} Fn (On \times On) \to dom ↑_{𝑜} = On \times On$
4	2 3	ax-mp	$⊢ dom ↑_{𝑜} = On \times On$
5	4	ndmov	$⊢ \neg (ω \in On \land C \in On) \to ω ↑_{𝑜} C = \emptyset$
6	1 5	nsyl2	$⊢ A \in (ω ↑_{𝑜} C) \to (ω \in On \land C \in On)$
7	6	ad2antrr	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to (ω \in On \land C \in On)$
8		oecl	$⊢ (ω \in On \land C \in On) \to ω ↑_{𝑜} C \in On$
9	7 8	syl	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to ω ↑_{𝑜} C \in On$
10		simplr	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to B \in On$
11		simpr	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to ω ↑_{𝑜} C \subseteq B$
12		oawordeu	$⊢ ((ω ↑_{𝑜} C \in On \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to \exists! x \in On (ω ↑_{𝑜} C) +_{𝑜} x = B$
13	9 10 11 12	syl21anc	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to \exists! x \in On (ω ↑_{𝑜} C) +_{𝑜} x = B$
14		reurex	$⊢ \exists! x \in On (ω ↑_{𝑜} C) +_{𝑜} x = B \to \exists x \in On (ω ↑_{𝑜} C) +_{𝑜} x = B$
15	13 14	syl	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to \exists x \in On (ω ↑_{𝑜} C) +_{𝑜} x = B$
16		simpll	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to A \in (ω ↑_{𝑜} C)$
17		onelon	$⊢ (ω ↑_{𝑜} C \in On \land A \in (ω ↑_{𝑜} C)) \to A \in On$
18	9 16 17	syl2anc	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to A \in On$
19	18	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to A \in On$
20	9	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to ω ↑_{𝑜} C \in On$
21		simpr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to x \in On$
22		oaass	$⊢ (A \in On \land ω ↑_{𝑜} C \in On \land x \in On) \to (A +_{𝑜} (ω ↑_{𝑜} C)) +_{𝑜} x = A +_{𝑜} ((ω ↑_{𝑜} C) +_{𝑜} x)$
23	19 20 21 22	syl3anc	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to (A +_{𝑜} (ω ↑_{𝑜} C)) +_{𝑜} x = A +_{𝑜} ((ω ↑_{𝑜} C) +_{𝑜} x)$
24	7	simprd	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to C \in On$
25		eloni	$⊢ C \in On \to Ord C$
26	24 25	syl	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to Ord C$
27		ordzsl	$⊢ Ord C \leftrightarrow (C = \emptyset \lor \exists x \in On C = suc x \lor Lim C)$
28	26 27	sylib	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to (C = \emptyset \lor \exists x \in On C = suc x \lor Lim C)$
29		simplll	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to A \in (ω ↑_{𝑜} C)$
30		oveq2	$⊢ C = \emptyset \to ω ↑_{𝑜} C = ω ↑_{𝑜} \emptyset$
31	7	simpld	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to ω \in On$
32		oe0	$⊢ ω \in On \to ω ↑_{𝑜} \emptyset = 1_{𝑜}$
33	31 32	syl	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to ω ↑_{𝑜} \emptyset = 1_{𝑜}$
34	30 33	sylan9eqr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to ω ↑_{𝑜} C = 1_{𝑜}$
35	29 34	eleqtrd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to A \in 1_{𝑜}$
36		el1o	$⊢ A \in 1_{𝑜} \leftrightarrow A = \emptyset$
37	35 36	sylib	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to A = \emptyset$
38	37	oveq1d	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to A +_{𝑜} (ω ↑_{𝑜} C) = \emptyset +_{𝑜} (ω ↑_{𝑜} C)$
39	9	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to ω ↑_{𝑜} C \in On$
40		oa0r	$⊢ ω ↑_{𝑜} C \in On \to \emptyset +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
41	39 40	syl	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to \emptyset +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
42	38 41	eqtrd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land C = \emptyset) \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
43	42	ex	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to (C = \emptyset \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C)$
44	31	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to ω \in On$
45		simprl	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to x \in On$
46		oecl	$⊢ (ω \in On \land x \in On) \to ω ↑_{𝑜} x \in On$
47	44 45 46	syl2anc	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to ω ↑_{𝑜} x \in On$
48		limom	$⊢ Lim ω$
49	44 48	jctir	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to (ω \in On \land Lim ω)$
50		simplll	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to A \in (ω ↑_{𝑜} C)$
51		simprr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to C = suc x$
52	51	oveq2d	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to ω ↑_{𝑜} C = ω ↑_{𝑜} suc x$
53		oesuc	$⊢ (ω \in On \land x \in On) \to ω ↑_{𝑜} suc x = (ω ↑_{𝑜} x) \cdot_{𝑜} ω$
54	44 45 53	syl2anc	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to ω ↑_{𝑜} suc x = (ω ↑_{𝑜} x) \cdot_{𝑜} ω$
55	52 54	eqtrd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to ω ↑_{𝑜} C = (ω ↑_{𝑜} x) \cdot_{𝑜} ω$
56	50 55	eleqtrd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} ω)$
57		omordlim	$⊢ ((ω ↑_{𝑜} x \in On \land (ω \in On \land Lim ω)) \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} ω)) \to \exists y \in ω A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y)$
58	47 49 56 57	syl21anc	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to \exists y \in ω A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y)$
59	47	adantr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ω ↑_{𝑜} x \in On$
60		nnon	$⊢ y \in ω \to y \in On$
61	60	ad2antrl	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to y \in On$
62		omcl	$⊢ (ω ↑_{𝑜} x \in On \land y \in On) \to (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On$
63	59 61 62	syl2anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On$
64		eloni	$⊢ (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On \to Ord ((ω ↑_{𝑜} x) \cdot_{𝑜} y)$
65	63 64	syl	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to Ord ((ω ↑_{𝑜} x) \cdot_{𝑜} y)$
66		simprr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y)$
67		ordelss	$⊢ (Ord ((ω ↑_{𝑜} x) \cdot_{𝑜} y) \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y)) \to A \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y$
68	65 66 67	syl2anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to A \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y$
69	18	ad2antrr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to A \in On$
70	9	ad2antrr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ω ↑_{𝑜} C \in On$
71		oawordri	$⊢ (A \in On \land (ω ↑_{𝑜} x) \cdot_{𝑜} y \in On \land ω ↑_{𝑜} C \in On) \to (A \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} C))$
72	69 63 70 71	syl3anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to (A \subseteq (ω ↑_{𝑜} x) \cdot_{𝑜} y \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} C))$
73	68 72	mpd	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} C)$
74	44	adantr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ω \in On$
75		odi	$⊢ (ω ↑_{𝑜} x \in On \land y \in On \land ω \in On) \to (ω ↑_{𝑜} x) \cdot_{𝑜} (y +_{𝑜} ω) = ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} ((ω ↑_{𝑜} x) \cdot_{𝑜} ω)$
76	59 61 74 75	syl3anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to (ω ↑_{𝑜} x) \cdot_{𝑜} (y +_{𝑜} ω) = ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} ((ω ↑_{𝑜} x) \cdot_{𝑜} ω)$
77		simprl	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to y \in ω$
78		oaabslem	$⊢ (ω \in On \land y \in ω) \to y +_{𝑜} ω = ω$
79	74 77 78	syl2anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to y +_{𝑜} ω = ω$
80	79	oveq2d	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to (ω ↑_{𝑜} x) \cdot_{𝑜} (y +_{𝑜} ω) = (ω ↑_{𝑜} x) \cdot_{𝑜} ω$
81	76 80	eqtr3d	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} ((ω ↑_{𝑜} x) \cdot_{𝑜} ω) = (ω ↑_{𝑜} x) \cdot_{𝑜} ω$
82	55	adantr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ω ↑_{𝑜} C = (ω ↑_{𝑜} x) \cdot_{𝑜} ω$
83	82	oveq2d	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} C) = ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} ((ω ↑_{𝑜} x) \cdot_{𝑜} ω)$
84	81 83 82	3eqtr4d	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to ((ω ↑_{𝑜} x) \cdot_{𝑜} y) +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
85	73 84	sseqtrd	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \land (y \in ω \land A \in ((ω ↑_{𝑜} x) \cdot_{𝑜} y))) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C$
86	58 85	rexlimddv	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C$
87		oaword2	$⊢ (ω ↑_{𝑜} C \in On \land A \in On) \to ω ↑_{𝑜} C \subseteq A +_{𝑜} (ω ↑_{𝑜} C)$
88	9 18 87	syl2anc	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to ω ↑_{𝑜} C \subseteq A +_{𝑜} (ω ↑_{𝑜} C)$
89	88	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to ω ↑_{𝑜} C \subseteq A +_{𝑜} (ω ↑_{𝑜} C)$
90	86 89	eqssd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land (x \in On \land C = suc x)) \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
91	90	rexlimdvaa	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to (\exists x \in On C = suc x \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C)$
92		simplll	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to A \in (ω ↑_{𝑜} C)$
93	31	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to ω \in On$
94	24	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to C \in On$
95		simpr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to Lim C$
96		oelim2	$⊢ (ω \in On \land (C \in On \land Lim C)) \to ω ↑_{𝑜} C = ⋃_{x \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} x)$
97	93 94 95 96	syl12anc	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to ω ↑_{𝑜} C = ⋃_{x \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} x)$
98	92 97	eleqtrd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to A \in ⋃_{x \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} x)$
99		eliun	$⊢ A \in ⋃_{x \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} x) \leftrightarrow \exists x \in (C ∖ 1_{𝑜}) A \in (ω ↑_{𝑜} x)$
100	98 99	sylib	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to \exists x \in (C ∖ 1_{𝑜}) A \in (ω ↑_{𝑜} x)$
101		eldifi	$⊢ x \in (C ∖ 1_{𝑜}) \to x \in C$
102	18	ad2antrr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to A \in On$
103	9	ad2antrr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to ω ↑_{𝑜} C \in On$
104	93	adantr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to ω \in On$
105		1onn	$⊢ 1_{𝑜} \in ω$
106		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
107	104 105 106	sylanblrc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to ω \in (On ∖ 2_{𝑜})$
108	94	adantr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to C \in On$
109		simplr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to Lim C$
110		oelimcl	$⊢ (ω \in (On ∖ 2_{𝑜}) \land (C \in On \land Lim C)) \to Lim (ω ↑_{𝑜} C)$
111	107 108 109 110	syl12anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to Lim (ω ↑_{𝑜} C)$
112		oalim	$⊢ (A \in On \land (ω ↑_{𝑜} C \in On \land Lim (ω ↑_{𝑜} C))) \to A +_{𝑜} (ω ↑_{𝑜} C) = ⋃_{y \in ω ↑_{𝑜} C} (A +_{𝑜} y)$
113	102 103 111 112	syl12anc	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to A +_{𝑜} (ω ↑_{𝑜} C) = ⋃_{y \in ω ↑_{𝑜} C} (A +_{𝑜} y)$
114		oelim2	$⊢ (ω \in On \land (C \in On \land Lim C)) \to ω ↑_{𝑜} C = ⋃_{z \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} z)$
115	93 94 95 114	syl12anc	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to ω ↑_{𝑜} C = ⋃_{z \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} z)$
116	115	eleq2d	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to (y \in (ω ↑_{𝑜} C) \leftrightarrow y \in ⋃_{z \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} z))$
117		eliun	$⊢ y \in ⋃_{z \in C ∖ 1_{𝑜}} (ω ↑_{𝑜} z) \leftrightarrow \exists z \in (C ∖ 1_{𝑜}) y \in (ω ↑_{𝑜} z)$
118	116 117	bitrdi	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to (y \in (ω ↑_{𝑜} C) \leftrightarrow \exists z \in (C ∖ 1_{𝑜}) y \in (ω ↑_{𝑜} z))$
119	118	adantr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to (y \in (ω ↑_{𝑜} C) \leftrightarrow \exists z \in (C ∖ 1_{𝑜}) y \in (ω ↑_{𝑜} z))$
120		eldifi	$⊢ z \in (C ∖ 1_{𝑜}) \to z \in C$
121	104	adantr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω \in On$
122	108	adantr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to C \in On$
123		simplrl	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to x \in C$
124		onelon	$⊢ (C \in On \land x \in C) \to x \in On$
125	122 123 124	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to x \in On$
126	121 125 46	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} x \in On$
127		eloni	$⊢ ω ↑_{𝑜} x \in On \to Ord (ω ↑_{𝑜} x)$
128	126 127	syl	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to Ord (ω ↑_{𝑜} x)$
129		simplrr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A \in (ω ↑_{𝑜} x)$
130		ordelss	$⊢ (Ord (ω ↑_{𝑜} x) \land A \in (ω ↑_{𝑜} x)) \to A \subseteq ω ↑_{𝑜} x$
131	128 129 130	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A \subseteq ω ↑_{𝑜} x$
132		ssun1	$⊢ x \subseteq x \cup z$
133	26	ad3antrrr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to Ord C$
134		simprl	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to z \in C$
135		ordunel	$⊢ (Ord C \land x \in C \land z \in C) \to x \cup z \in C$
136	133 123 134 135	syl3anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to x \cup z \in C$
137		onelon	$⊢ (C \in On \land x \cup z \in C) \to x \cup z \in On$
138	122 136 137	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to x \cup z \in On$
139		peano1	$⊢ \emptyset \in ω$
140	139	a1i	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to \emptyset \in ω$
141		oewordi	$⊢ ((x \in On \land x \cup z \in On \land ω \in On) \land \emptyset \in ω) \to (x \subseteq x \cup z \to ω ↑_{𝑜} x \subseteq ω ↑_{𝑜} (x \cup z))$
142	125 138 121 140 141	syl31anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (x \subseteq x \cup z \to ω ↑_{𝑜} x \subseteq ω ↑_{𝑜} (x \cup z))$
143	132 142	mpi	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} x \subseteq ω ↑_{𝑜} (x \cup z)$
144	131 143	sstrd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A \subseteq ω ↑_{𝑜} (x \cup z)$
145	102	adantr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A \in On$
146		oecl	$⊢ (ω \in On \land x \cup z \in On) \to ω ↑_{𝑜} (x \cup z) \in On$
147	121 138 146	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} (x \cup z) \in On$
148		onelon	$⊢ (C \in On \land z \in C) \to z \in On$
149	122 134 148	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to z \in On$
150		oecl	$⊢ (ω \in On \land z \in On) \to ω ↑_{𝑜} z \in On$
151	121 149 150	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} z \in On$
152		simprr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to y \in (ω ↑_{𝑜} z)$
153		onelon	$⊢ (ω ↑_{𝑜} z \in On \land y \in (ω ↑_{𝑜} z)) \to y \in On$
154	151 152 153	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to y \in On$
155		oawordri	$⊢ (A \in On \land ω ↑_{𝑜} (x \cup z) \in On \land y \in On) \to (A \subseteq ω ↑_{𝑜} (x \cup z) \to A +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} y)$
156	145 147 154 155	syl3anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (A \subseteq ω ↑_{𝑜} (x \cup z) \to A +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} y)$
157	144 156	mpd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} y$
158		eloni	$⊢ ω ↑_{𝑜} z \in On \to Ord (ω ↑_{𝑜} z)$
159	151 158	syl	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to Ord (ω ↑_{𝑜} z)$
160		ordelss	$⊢ (Ord (ω ↑_{𝑜} z) \land y \in (ω ↑_{𝑜} z)) \to y \subseteq ω ↑_{𝑜} z$
161	159 152 160	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to y \subseteq ω ↑_{𝑜} z$
162		ssun2	$⊢ z \subseteq x \cup z$
163		oewordi	$⊢ ((z \in On \land x \cup z \in On \land ω \in On) \land \emptyset \in ω) \to (z \subseteq x \cup z \to ω ↑_{𝑜} z \subseteq ω ↑_{𝑜} (x \cup z))$
164	149 138 121 140 163	syl31anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (z \subseteq x \cup z \to ω ↑_{𝑜} z \subseteq ω ↑_{𝑜} (x \cup z))$
165	162 164	mpi	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} z \subseteq ω ↑_{𝑜} (x \cup z)$
166	161 165	sstrd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to y \subseteq ω ↑_{𝑜} (x \cup z)$
167		oaword	$⊢ (y \in On \land ω ↑_{𝑜} (x \cup z) \in On \land ω ↑_{𝑜} (x \cup z) \in On) \to (y \subseteq ω ↑_{𝑜} (x \cup z) \leftrightarrow (ω ↑_{𝑜} (x \cup z)) +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z)))$
168	154 147 147 167	syl3anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (y \subseteq ω ↑_{𝑜} (x \cup z) \leftrightarrow (ω ↑_{𝑜} (x \cup z)) +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z)))$
169	166 168	mpbid	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (ω ↑_{𝑜} (x \cup z)) +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z))$
170	157 169	sstrd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A +_{𝑜} y \subseteq (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z))$
171		ordom	$⊢ Ord ω$
172		ordsucss	$⊢ Ord ω \to (1_{𝑜} \in ω \to suc 1_{𝑜} \subseteq ω)$
173	171 105 172	mp2	$⊢ suc 1_{𝑜} \subseteq ω$
174		1on	$⊢ 1_{𝑜} \in On$
175		onsuc	$⊢ 1_{𝑜} \in On \to suc 1_{𝑜} \in On$
176	174 175	mp1i	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to suc 1_{𝑜} \in On$
177		omwordi	$⊢ (suc 1_{𝑜} \in On \land ω \in On \land ω ↑_{𝑜} (x \cup z) \in On) \to (suc 1_{𝑜} \subseteq ω \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} suc 1_{𝑜} \subseteq (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} ω)$
178	176 121 147 177	syl3anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (suc 1_{𝑜} \subseteq ω \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} suc 1_{𝑜} \subseteq (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} ω)$
179	173 178	mpi	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} suc 1_{𝑜} \subseteq (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} ω$
180	174	a1i	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to 1_{𝑜} \in On$
181		omsuc	$⊢ (ω ↑_{𝑜} (x \cup z) \in On \land 1_{𝑜} \in On) \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} suc 1_{𝑜} = ((ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} (ω ↑_{𝑜} (x \cup z))$
182	147 180 181	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} suc 1_{𝑜} = ((ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} (ω ↑_{𝑜} (x \cup z))$
183		om1	$⊢ ω ↑_{𝑜} (x \cup z) \in On \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} 1_{𝑜} = ω ↑_{𝑜} (x \cup z)$
184	147 183	syl	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} 1_{𝑜} = ω ↑_{𝑜} (x \cup z)$
185	184	oveq1d	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ((ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} 1_{𝑜}) +_{𝑜} (ω ↑_{𝑜} (x \cup z)) = (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z))$
186	182 185	eqtr2d	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z)) = (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} suc 1_{𝑜}$
187		oesuc	$⊢ (ω \in On \land x \cup z \in On) \to ω ↑_{𝑜} suc (x \cup z) = (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} ω$
188	121 138 187	syl2anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} suc (x \cup z) = (ω ↑_{𝑜} (x \cup z)) \cdot_{𝑜} ω$
189	179 186 188	3sstr4d	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (ω ↑_{𝑜} (x \cup z)) +_{𝑜} (ω ↑_{𝑜} (x \cup z)) \subseteq ω ↑_{𝑜} suc (x \cup z)$
190	170 189	sstrd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A +_{𝑜} y \subseteq ω ↑_{𝑜} suc (x \cup z)$
191		ordsucss	$⊢ Ord C \to (x \cup z \in C \to suc (x \cup z) \subseteq C)$
192	133 136 191	sylc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to suc (x \cup z) \subseteq C$
193		onsuc	$⊢ x \cup z \in On \to suc (x \cup z) \in On$
194	138 193	syl	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to suc (x \cup z) \in On$
195		oewordi	$⊢ ((suc (x \cup z) \in On \land C \in On \land ω \in On) \land \emptyset \in ω) \to (suc (x \cup z) \subseteq C \to ω ↑_{𝑜} suc (x \cup z) \subseteq ω ↑_{𝑜} C)$
196	194 122 121 140 195	syl31anc	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to (suc (x \cup z) \subseteq C \to ω ↑_{𝑜} suc (x \cup z) \subseteq ω ↑_{𝑜} C)$
197	192 196	mpd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to ω ↑_{𝑜} suc (x \cup z) \subseteq ω ↑_{𝑜} C$
198	190 197	sstrd	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land (z \in C \land y \in (ω ↑_{𝑜} z))) \to A +_{𝑜} y \subseteq ω ↑_{𝑜} C$
199	198	expr	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land z \in C) \to (y \in (ω ↑_{𝑜} z) \to A +_{𝑜} y \subseteq ω ↑_{𝑜} C)$
200	120 199	sylan2	$⊢ (((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \land z \in (C ∖ 1_{𝑜})) \to (y \in (ω ↑_{𝑜} z) \to A +_{𝑜} y \subseteq ω ↑_{𝑜} C)$
201	200	rexlimdva	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to (\exists z \in (C ∖ 1_{𝑜}) y \in (ω ↑_{𝑜} z) \to A +_{𝑜} y \subseteq ω ↑_{𝑜} C)$
202	119 201	sylbid	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to (y \in (ω ↑_{𝑜} C) \to A +_{𝑜} y \subseteq ω ↑_{𝑜} C)$
203	202	ralrimiv	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to \forall y \in (ω ↑_{𝑜} C) A +_{𝑜} y \subseteq ω ↑_{𝑜} C$
204		iunss	$⊢ ⋃_{y \in ω ↑_{𝑜} C} (A +_{𝑜} y) \subseteq ω ↑_{𝑜} C \leftrightarrow \forall y \in (ω ↑_{𝑜} C) A +_{𝑜} y \subseteq ω ↑_{𝑜} C$
205	203 204	sylibr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to ⋃_{y \in ω ↑_{𝑜} C} (A +_{𝑜} y) \subseteq ω ↑_{𝑜} C$
206	113 205	eqsstrd	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land (x \in C \land A \in (ω ↑_{𝑜} x))) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C$
207	206	expr	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land x \in C) \to (A \in (ω ↑_{𝑜} x) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C)$
208	101 207	sylan2	$⊢ ((((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \land x \in (C ∖ 1_{𝑜})) \to (A \in (ω ↑_{𝑜} x) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C)$
209	208	rexlimdva	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to (\exists x \in (C ∖ 1_{𝑜}) A \in (ω ↑_{𝑜} x) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C)$
210	100 209	mpd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to A +_{𝑜} (ω ↑_{𝑜} C) \subseteq ω ↑_{𝑜} C$
211	88	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to ω ↑_{𝑜} C \subseteq A +_{𝑜} (ω ↑_{𝑜} C)$
212	210 211	eqssd	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land Lim C) \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
213	212	ex	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to (Lim C \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C)$
214	43 91 213	3jaod	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to ((C = \emptyset \lor \exists x \in On C = suc x \lor Lim C) \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C)$
215	28 214	mpd	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
216	215	adantr	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to A +_{𝑜} (ω ↑_{𝑜} C) = ω ↑_{𝑜} C$
217	216	oveq1d	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to (A +_{𝑜} (ω ↑_{𝑜} C)) +_{𝑜} x = (ω ↑_{𝑜} C) +_{𝑜} x$
218	23 217	eqtr3d	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to A +_{𝑜} ((ω ↑_{𝑜} C) +_{𝑜} x) = (ω ↑_{𝑜} C) +_{𝑜} x$
219		oveq2	$⊢ (ω ↑_{𝑜} C) +_{𝑜} x = B \to A +_{𝑜} ((ω ↑_{𝑜} C) +_{𝑜} x) = A +_{𝑜} B$
220		id	$⊢ (ω ↑_{𝑜} C) +_{𝑜} x = B \to (ω ↑_{𝑜} C) +_{𝑜} x = B$
221	219 220	eqeq12d	$⊢ (ω ↑_{𝑜} C) +_{𝑜} x = B \to (A +_{𝑜} ((ω ↑_{𝑜} C) +_{𝑜} x) = (ω ↑_{𝑜} C) +_{𝑜} x \leftrightarrow A +_{𝑜} B = B)$
222	218 221	syl5ibcom	$⊢ (((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \land x \in On) \to ((ω ↑_{𝑜} C) +_{𝑜} x = B \to A +_{𝑜} B = B)$
223	222	rexlimdva	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to (\exists x \in On (ω ↑_{𝑜} C) +_{𝑜} x = B \to A +_{𝑜} B = B)$
224	15 223	mpd	$⊢ ((A \in (ω ↑_{𝑜} C) \land B \in On) \land ω ↑_{𝑜} C \subseteq B) \to A +_{𝑜} B = B$

Metamath Proof Explorer

Theorem oaabs2

Proof