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	⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω )
Assertion	unblem4	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐹 : ω –1-1→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		unblem.2	⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω )
2		omsson	⊢ ω ⊆ On
3		sstr	⊢ ( ( 𝐴 ⊆ ω ∧ ω ⊆ On ) → 𝐴 ⊆ On )
4	2 3	mpan2	⊢ ( 𝐴 ⊆ ω → 𝐴 ⊆ On )
5	4	adantr	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐴 ⊆ On )
6		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) Fn ω
7	1	fneq1i	⊢ ( 𝐹 Fn ω ↔ ( rec ( ( 𝑥 ∈ V ↦ ∩ ( 𝐴 ∖ suc 𝑥 ) ) , ∩ 𝐴 ) ↾ ω ) Fn ω )
8	6 7	mpbir	⊢ 𝐹 Fn ω
9	1	unblem2	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) )
10	9	ralrimiv	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 )
11		ffnfv	⊢ ( 𝐹 : ω ⟶ 𝐴 ↔ ( 𝐹 Fn ω ∧ ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) )
12	11	biimpri	⊢ ( ( 𝐹 Fn ω ∧ ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ 𝐴 ) → 𝐹 : ω ⟶ 𝐴 )
13	8 10 12	sylancr	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐹 : ω ⟶ 𝐴 )
14	1	unblem3	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ( 𝑧 ∈ ω → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) ) )
15	14	ralrimiv	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) )
16		omsmo	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑧 ∈ ω ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑧 ) ) → 𝐹 : ω –1-1→ 𝐴 )
17	5 13 15 16	syl21anc	⊢ ( ( 𝐴 ⊆ ω ∧ ∀ 𝑤 ∈ ω ∃ 𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ) → 𝐹 : ω –1-1→ 𝐴 )