Metamath Proof Explorer

Theorem unblem4

Description: Lemma for unbnn . The function F maps the set of natural numbers one-to-one to the set of unbounded natural numbers A . (Contributed by NM, 3-Dec-2003)

		Ref	Expression
	Hypothesis	unblem.2	$⊢ F = {rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}$
	Assertion	unblem4	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to F : ω \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		unblem.2	$⊢ F = {rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}$
2		omsson	$⊢ ω \subseteq On$
3		sstr	$⊢ (A \subseteq ω \land ω \subseteq On) \to A \subseteq On$
4	2 3	mpan2	$⊢ A \subseteq ω \to A \subseteq On$
5	4	adantr	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to A \subseteq On$
6		frfnom	$⊢ ({rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}) Fn ω$
7	1	fneq1i	$⊢ F Fn ω \leftrightarrow ({rec ((x \in V ⟼ ⋂ (A ∖ suc x)), ⋂ A) ↾}_{ω}) Fn ω$
8	6 7	mpbir	$⊢ F Fn ω$
9	1	unblem2	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (z) \in A)$
10	9	ralrimiv	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to \forall z \in ω F (z) \in A$
11		ffnfv	$⊢ F : ω ⟶ A \leftrightarrow (F Fn ω \land \forall z \in ω F (z) \in A)$
12	11	biimpri	$⊢ (F Fn ω \land \forall z \in ω F (z) \in A) \to F : ω ⟶ A$
13	8 10 12	sylancr	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to F : ω ⟶ A$
14	1	unblem3	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to (z \in ω \to F (z) \in F (suc z))$
15	14	ralrimiv	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to \forall z \in ω F (z) \in F (suc z)$
16		omsmo	$⊢ ((A \subseteq On \land F : ω ⟶ A) \land \forall z \in ω F (z) \in F (suc z)) \to F : ω \underset{1-1}{⟶} A$
17	5 13 15 16	syl21anc	$⊢ (A \subseteq ω \land \forall w \in ω \exists v \in A w \in v) \to F : ω \underset{1-1}{⟶} A$