oaabslem

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

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		limom	$⊢ Lim ω$
3	2	jctr	$⊢ ω \in On \to (ω \in On \land Lim ω)$
4		oalim	$⊢ (A \in On \land (ω \in On \land Lim ω)) \to A +_{𝑜} ω = ⋃_{x \in ω} (A +_{𝑜} x)$
5	1 3 4	syl2an	$⊢ (A \in ω \land ω \in On) \to A +_{𝑜} ω = ⋃_{x \in ω} (A +_{𝑜} x)$
6		ordom	$⊢ Ord ω$
7		nnacl	$⊢ (A \in ω \land x \in ω) \to A +_{𝑜} x \in ω$
8		ordelss	$⊢ (Ord ω \land A +_{𝑜} x \in ω) \to A +_{𝑜} x \subseteq ω$
9	6 7 8	sylancr	$⊢ (A \in ω \land x \in ω) \to A +_{𝑜} x \subseteq ω$
10	9	ralrimiva	$⊢ A \in ω \to \forall x \in ω A +_{𝑜} x \subseteq ω$
11		iunss	$⊢ ⋃_{x \in ω} (A +_{𝑜} x) \subseteq ω \leftrightarrow \forall x \in ω A +_{𝑜} x \subseteq ω$
12	10 11	sylibr	$⊢ A \in ω \to ⋃_{x \in ω} (A +_{𝑜} x) \subseteq ω$
13	12	adantr	$⊢ (A \in ω \land ω \in On) \to ⋃_{x \in ω} (A +_{𝑜} x) \subseteq ω$
14	5 13	eqsstrd	$⊢ (A \in ω \land ω \in On) \to A +_{𝑜} ω \subseteq ω$
15	14	ancoms	$⊢ (ω \in On \land A \in ω) \to A +_{𝑜} ω \subseteq ω$
16		oaword2	$⊢ (ω \in On \land A \in On) \to ω \subseteq A +_{𝑜} ω$
17	1 16	sylan2	$⊢ (ω \in On \land A \in ω) \to ω \subseteq A +_{𝑜} ω$
18	15 17	eqssd	$⊢ (ω \in On \land A \in ω) \to A +_{𝑜} ω = ω$

Metamath Proof Explorer