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 𝐹 = ( 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𝐴 )