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 
|- ( ( A ~<_ _om /\ A =/= (/) ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )

Proof

Step Hyp Ref Expression
1 nnfoctb 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> E. g g : NN -onto-> A )
2 fofn 
 |-  ( g : NN -onto-> A -> g Fn NN )
3 nnex 
 |-  NN e. _V
4 3 a1i 
 |-  ( g : NN -onto-> A -> NN e. _V )
5 ltwenn 
 |-  < We NN
6 5 a1i 
 |-  ( g : NN -onto-> A -> < We NN )
7 2 4 6 wessf1orn 
 |-  ( g : NN -onto-> A -> E. x e. ~P NN ( g |` x ) : x -1-1-onto-> ran g )
8 f1odm 
 |-  ( ( g |` x ) : x -1-1-onto-> ran g -> dom ( g |` x ) = x )
9 8 adantl 
 |-  ( ( x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> dom ( g |` x ) = x )
10 elpwi 
 |-  ( x e. ~P NN -> x C_ NN )
11 10 adantr 
 |-  ( ( x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> x C_ NN )
12 9 11 eqsstrd 
 |-  ( ( x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> dom ( g |` x ) C_ NN )
13 12 3adant1 
 |-  ( ( g : NN -onto-> A /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> dom ( g |` x ) C_ NN )
14 simpr 
 |-  ( ( g : NN -onto-> A /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : x -1-1-onto-> ran g )
15 eqidd 
 |-  ( ( g : NN -onto-> A /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) = ( g |` x ) )
16 8 eqcomd 
 |-  ( ( g |` x ) : x -1-1-onto-> ran g -> x = dom ( g |` x ) )
17 16 adantl 
 |-  ( ( g : NN -onto-> A /\ ( g |` x ) : x -1-1-onto-> ran g ) -> x = dom ( g |` x ) )
18 forn 
 |-  ( g : NN -onto-> A -> ran g = A )
19 18 adantr 
 |-  ( ( g : NN -onto-> A /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ran g = A )
20 15 17 19 f1oeq123d 
 |-  ( ( g : NN -onto-> A /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( ( g |` x ) : x -1-1-onto-> ran g <-> ( g |` x ) : dom ( g |` x ) -1-1-onto-> A ) )
21 14 20 mpbid 
 |-  ( ( g : NN -onto-> A /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : dom ( g |` x ) -1-1-onto-> A )
22 21 3adant2 
 |-  ( ( g : NN -onto-> A /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : dom ( g |` x ) -1-1-onto-> A )
23 vex 
 |-  g e. _V
24 23 resex 
 |-  ( g |` x ) e. _V
25 dmeq 
 |-  ( f = ( g |` x ) -> dom f = dom ( g |` x ) )
26 25 sseq1d 
 |-  ( f = ( g |` x ) -> ( dom f C_ NN <-> dom ( g |` x ) C_ NN ) )
27 id 
 |-  ( f = ( g |` x ) -> f = ( g |` x ) )
28 eqidd 
 |-  ( f = ( g |` x ) -> A = A )
29 27 25 28 f1oeq123d 
 |-  ( f = ( g |` x ) -> ( f : dom f -1-1-onto-> A <-> ( g |` x ) : dom ( g |` x ) -1-1-onto-> A ) )
30 26 29 anbi12d 
 |-  ( f = ( g |` x ) -> ( ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) <-> ( dom ( g |` x ) C_ NN /\ ( g |` x ) : dom ( g |` x ) -1-1-onto-> A ) ) )
31 24 30 spcev 
 |-  ( ( dom ( g |` x ) C_ NN /\ ( g |` x ) : dom ( g |` x ) -1-1-onto-> A ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )
32 13 22 31 syl2anc 
 |-  ( ( g : NN -onto-> A /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )
33 32 3exp 
 |-  ( g : NN -onto-> A -> ( x e. ~P NN -> ( ( g |` x ) : x -1-1-onto-> ran g -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) ) ) )
34 33 rexlimdv 
 |-  ( g : NN -onto-> A -> ( E. x e. ~P NN ( g |` x ) : x -1-1-onto-> ran g -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) ) )
35 7 34 mpd 
 |-  ( g : NN -onto-> A -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )
36 35 a1i 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> ( g : NN -onto-> A -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) ) )
37 36 exlimdv 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> ( E. g g : NN -onto-> A -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) ) )
38 1 37 mpd 
 |-  ( ( A ~<_ _om /\ A =/= (/) ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )