This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackbij1lem3

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

		Ref	Expression
	Assertion	ackbij1lem3	$⊢ A \in ω \to A \in (𝒫 ω \cap Fin)$

Step	Hyp	Ref	Expression
1		ordom	$⊢ Ord ω$
2		ordelss	$⊢ (Ord ω \land A \in ω) \to A \subseteq ω$
3	1 2	mpan	$⊢ A \in ω \to A \subseteq ω$
4		elpwg	$⊢ A \in ω \to (A \in 𝒫 ω \leftrightarrow A \subseteq ω)$
5	3 4	mpbird	$⊢ A \in ω \to A \in 𝒫 ω$
6		nnfi	$⊢ A \in ω \to A \in Fin$
7	5 6	elind	$⊢ A \in ω \to A \in (𝒫 ω \cap Fin)$