omabslem

		Ref	Expression
	Assertion	omabslem	$⊢ (ω \in On \land A \in ω \land \emptyset \in A) \to A \cdot_{𝑜} ω = ω$

Proof

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		omlim	$⊢ (A \in On \land (ω \in On \land Lim ω)) \to A \cdot_{𝑜} ω = ⋃_{x \in ω} (A \cdot_{𝑜} x)$
5	1 3 4	syl2an	$⊢ (A \in ω \land ω \in On) \to A \cdot_{𝑜} ω = ⋃_{x \in ω} (A \cdot_{𝑜} x)$
6		ordom	$⊢ Ord ω$
7		nnmcl	$⊢ (A \in ω \land x \in ω) \to A \cdot_{𝑜} x \in ω$
8		ordelss	$⊢ (Ord ω \land A \cdot_{𝑜} x \in ω) \to A \cdot_{𝑜} x \subseteq ω$
9	6 7 8	sylancr	$⊢ (A \in ω \land x \in ω) \to A \cdot_{𝑜} x \subseteq ω$
10	9	ralrimiva	$⊢ A \in ω \to \forall x \in ω A \cdot_{𝑜} x \subseteq ω$
11		iunss	$⊢ ⋃_{x \in ω} (A \cdot_{𝑜} x) \subseteq ω \leftrightarrow \forall x \in ω A \cdot_{𝑜} x \subseteq ω$
12	10 11	sylibr	$⊢ A \in ω \to ⋃_{x \in ω} (A \cdot_{𝑜} x) \subseteq ω$
13	12	adantr	$⊢ (A \in ω \land ω \in On) \to ⋃_{x \in ω} (A \cdot_{𝑜} x) \subseteq ω$
14	5 13	eqsstrd	$⊢ (A \in ω \land ω \in On) \to A \cdot_{𝑜} ω \subseteq ω$
15	14	ancoms	$⊢ (ω \in On \land A \in ω) \to A \cdot_{𝑜} ω \subseteq ω$
16	15	3adant3	$⊢ (ω \in On \land A \in ω \land \emptyset \in A) \to A \cdot_{𝑜} ω \subseteq ω$
17		omword2	$⊢ ((ω \in On \land A \in On) \land \emptyset \in A) \to ω \subseteq A \cdot_{𝑜} ω$
18	17	3impa	$⊢ (ω \in On \land A \in On \land \emptyset \in A) \to ω \subseteq A \cdot_{𝑜} ω$
19	1 18	syl3an2	$⊢ (ω \in On \land A \in ω \land \emptyset \in A) \to ω \subseteq A \cdot_{𝑜} ω$
20	16 19	eqssd	$⊢ (ω \in On \land A \in ω \land \emptyset \in A) \to A \cdot_{𝑜} ω = ω$

Metamath Proof Explorer

Theorem omabslem

Proof