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