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

Metamath Proof Explorer

Theorem ssnnf1octb

Description: There exists a bijection between a subset of NN and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion ssnnf1octb ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nnfoctb ⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 )
2 fofn ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → 𝑔 Fn ℕ )
3 nnex ⊢ ℕ ∈ V
4 3 a1i ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ℕ ∈ V )
5 ltwenn ⊢ < We ℕ
6 5 a1i ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → < We ℕ )
7 2 4 6 wessf1orn ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∃ 𝑥 ∈ 𝒫 ℕ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 )
8 f1odm ⊢ ( ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 → dom ( 𝑔 ↾ 𝑥 ) = 𝑥 )
9 8 adantl ⊢ ( ( 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → dom ( 𝑔 ↾ 𝑥 ) = 𝑥 )
10 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℕ → 𝑥 ⊆ ℕ )
11 10 adantr ⊢ ( ( 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → 𝑥 ⊆ ℕ )
12 9 11 eqsstrd ⊢ ( ( 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → dom ( 𝑔 ↾ 𝑥 ) ⊆ ℕ )
13 12 3adant1 ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → dom ( 𝑔 ↾ 𝑥 ) ⊆ ℕ )
14 simpr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 )
15 eqidd ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) = ( 𝑔 ↾ 𝑥 ) )
16 8 eqcomd ⊢ ( ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 → 𝑥 = dom ( 𝑔 ↾ 𝑥 ) )
17 16 adantl ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → 𝑥 = dom ( 𝑔 ↾ 𝑥 ) )
18 forn ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ran 𝑔 = 𝐴 )
19 18 adantr ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ran 𝑔 = 𝐴 )
20 15 17 19 f1oeq123d ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ↔ ( 𝑔 ↾ 𝑥 ) : dom ( 𝑔 ↾ 𝑥 ) –1-1-onto→ 𝐴 ) )
21 14 20 mpbid ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : dom ( 𝑔 ↾ 𝑥 ) –1-1-onto→ 𝐴 )
22 21 3adant2 ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : dom ( 𝑔 ↾ 𝑥 ) –1-1-onto→ 𝐴 )
23 vex ⊢ 𝑔 ∈ V
24 23 resex ⊢ ( 𝑔 ↾ 𝑥 ) ∈ V
25 dmeq ⊢ ( 𝑓 = ( 𝑔 ↾ 𝑥 ) → dom 𝑓 = dom ( 𝑔 ↾ 𝑥 ) )
26 25 sseq1d ⊢ ( 𝑓 = ( 𝑔 ↾ 𝑥 ) → ( dom 𝑓 ⊆ ℕ ↔ dom ( 𝑔 ↾ 𝑥 ) ⊆ ℕ ) )
27 id ⊢ ( 𝑓 = ( 𝑔 ↾ 𝑥 ) → 𝑓 = ( 𝑔 ↾ 𝑥 ) )
28 eqidd ⊢ ( 𝑓 = ( 𝑔 ↾ 𝑥 ) → 𝐴 = 𝐴 )
29 27 25 28 f1oeq123d ⊢ ( 𝑓 = ( 𝑔 ↾ 𝑥 ) → ( 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ↔ ( 𝑔 ↾ 𝑥 ) : dom ( 𝑔 ↾ 𝑥 ) –1-1-onto→ 𝐴 ) )
30 26 29 anbi12d ⊢ ( 𝑓 = ( 𝑔 ↾ 𝑥 ) → ( ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) ↔ ( dom ( 𝑔 ↾ 𝑥 ) ⊆ ℕ ∧ ( 𝑔 ↾ 𝑥 ) : dom ( 𝑔 ↾ 𝑥 ) –1-1-onto→ 𝐴 ) ) )
31 24 30 spcev ⊢ ( ( dom ( 𝑔 ↾ 𝑥 ) ⊆ ℕ ∧ ( 𝑔 ↾ 𝑥 ) : dom ( 𝑔 ↾ 𝑥 ) –1-1-onto→ 𝐴 ) → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) )
32 13 22 31 syl2anc ⊢ ( ( 𝑔 : ℕ –onto→ 𝐴 ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) )
33 32 3exp ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( 𝑥 ∈ 𝒫 ℕ → ( ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) ) ) )
34 33 rexlimdv ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ( ∃ 𝑥 ∈ 𝒫 ℕ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) ) )
35 7 34 mpd ⊢ ( 𝑔 : ℕ –onto→ 𝐴 → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) )
36 35 a1i ⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( 𝑔 : ℕ –onto→ 𝐴 → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) ) )
37 36 exlimdv ⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑔 𝑔 : ℕ –onto→ 𝐴 → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) ) )
38 1 37 mpd ⊢ ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 ( dom 𝑓 ⊆ ℕ ∧ 𝑓 : dom 𝑓 –1-1-onto→ 𝐴 ) )