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

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→ 𝐴 )