oaabs

Description: Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of TakeutiZaring p. 59. (Contributed by NM, 9-Dec-2004) (Proof shortened by Mario Carneiro, 29-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ssexg	$⊢ (ω \subseteq B \land B \in On) \to ω \in V$
2	1	ex	$⊢ ω \subseteq B \to (B \in On \to ω \in V)$
3		omelon2	$⊢ ω \in V \to ω \in On$
4	2 3	syl6com	$⊢ B \in On \to (ω \subseteq B \to ω \in On)$
5	4	imp	$⊢ (B \in On \land ω \subseteq B) \to ω \in On$
6	5	adantll	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to ω \in On$
7		simplr	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to B \in On$
8	6 7	jca	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to (ω \in On \land B \in On)$
9		oawordeu	$⊢ ((ω \in On \land B \in On) \land ω \subseteq B) \to \exists! x \in On ω +_{𝑜} x = B$
10	8 9	sylancom	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to \exists! x \in On ω +_{𝑜} x = B$
11		reurex	$⊢ \exists! x \in On ω +_{𝑜} x = B \to \exists x \in On ω +_{𝑜} x = B$
12	10 11	syl	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to \exists x \in On ω +_{𝑜} x = B$
13		nnon	$⊢ A \in ω \to A \in On$
14	13	ad3antrrr	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to A \in On$
15	6	adantr	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to ω \in On$
16		simpr	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to x \in On$
17		oaass	$⊢ (A \in On \land ω \in On \land x \in On) \to (A +_{𝑜} ω) +_{𝑜} x = A +_{𝑜} (ω +_{𝑜} x)$
18	14 15 16 17	syl3anc	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to (A +_{𝑜} ω) +_{𝑜} x = A +_{𝑜} (ω +_{𝑜} x)$
19		simpll	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to A \in ω$
20		oaabslem	$⊢ (ω \in On \land A \in ω) \to A +_{𝑜} ω = ω$
21	6 19 20	syl2anc	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to A +_{𝑜} ω = ω$
22	21	adantr	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to A +_{𝑜} ω = ω$
23	22	oveq1d	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to (A +_{𝑜} ω) +_{𝑜} x = ω +_{𝑜} x$
24	18 23	eqtr3d	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to A +_{𝑜} (ω +_{𝑜} x) = ω +_{𝑜} x$
25		oveq2	$⊢ ω +_{𝑜} x = B \to A +_{𝑜} (ω +_{𝑜} x) = A +_{𝑜} B$
26		id	$⊢ ω +_{𝑜} x = B \to ω +_{𝑜} x = B$
27	25 26	eqeq12d	$⊢ ω +_{𝑜} x = B \to (A +_{𝑜} (ω +_{𝑜} x) = ω +_{𝑜} x \leftrightarrow A +_{𝑜} B = B)$
28	24 27	syl5ibcom	$⊢ (((A \in ω \land B \in On) \land ω \subseteq B) \land x \in On) \to (ω +_{𝑜} x = B \to A +_{𝑜} B = B)$
29	28	rexlimdva	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to (\exists x \in On ω +_{𝑜} x = B \to A +_{𝑜} B = B)$
30	12 29	mpd	$⊢ ((A \in ω \land B \in On) \land ω \subseteq B) \to A +_{𝑜} B = B$

Metamath Proof Explorer

Theorem oaabs

Proof