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 ⊢ F = rec ⁡ x ∈ V ⟼ ⋂ A ∖ suc ⁡ x ⋂ A ↾ ω
Assertion unblem4 ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → F : ω ⟶ 1-1 A

Proof

Step Hyp Ref Expression
1 unblem.2 ⊢ F = rec ⁡ x ∈ V ⟼ ⋂ A ∖ suc ⁡ x ⋂ A ↾ ω
2 omsson ⊢ ω ⊆ On
3 sstr ⊢ A ⊆ ω ∧ ω ⊆ On → A ⊆ On
4 2 3 mpan2 ⊢ A ⊆ ω → A ⊆ On
5 4 adantr ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → A ⊆ On
6 frfnom ⊢ rec ⁡ x ∈ V ⟼ ⋂ A ∖ suc ⁡ x ⋂ A ↾ ω Fn ω
7 1 fneq1i ⊢ F Fn ω ↔ rec ⁡ x ∈ V ⟼ ⋂ A ∖ suc ⁡ x ⋂ A ↾ ω Fn ω
8 6 7 mpbir ⊢ F Fn ω
9 1 unblem2 ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → z ∈ ω → F ⁡ z ∈ A
10 9 ralrimiv ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → ∀ z ∈ ω F ⁡ z ∈ A
11 ffnfv ⊢ F : ω ⟶ A ↔ F Fn ω ∧ ∀ z ∈ ω F ⁡ z ∈ A
12 11 biimpri ⊢ F Fn ω ∧ ∀ z ∈ ω F ⁡ z ∈ A → F : ω ⟶ A
13 8 10 12 sylancr ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → F : ω ⟶ A
14 1 unblem3 ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → z ∈ ω → F ⁡ z ∈ F ⁡ suc ⁡ z
15 14 ralrimiv ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → ∀ z ∈ ω F ⁡ z ∈ F ⁡ suc ⁡ z
16 omsmo ⊢ A ⊆ On ∧ F : ω ⟶ A ∧ ∀ z ∈ ω F ⁡ z ∈ F ⁡ suc ⁡ z → F : ω ⟶ 1-1 A
17 5 13 15 16 syl21anc ⊢ A ⊆ ω ∧ ∀ w ∈ ω ∃ v ∈ A w ∈ v → F : ω ⟶ 1-1 A