Metamath Proof Explorer

Theorem nnfoctbdj

Description: There exists a mapping from NN onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses nnfoctbdj.ctb 
|- ( ph -> X ~<_ _om )
nnfoctbdj.n0 
|- ( ph -> X =/= (/) )
nnfoctbdj.dj 
|- ( ph -> Disj_ y e. X y )
Assertion nnfoctbdj 
|- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) )

Proof

Step Hyp Ref Expression
1 nnfoctbdj.ctb 
 |-  ( ph -> X ~<_ _om )
2 nnfoctbdj.n0 
 |-  ( ph -> X =/= (/) )
3 nnfoctbdj.dj 
 |-  ( ph -> Disj_ y e. X y )
4 nnfoctb 
 |-  ( ( X ~<_ _om /\ X =/= (/) ) -> E. g g : NN -onto-> X )
5 1 2 4 syl2anc 
 |-  ( ph -> E. g g : NN -onto-> X )
6 fofn 
 |-  ( g : NN -onto-> X -> g Fn NN )
7 6 adantl 
 |-  ( ( ph /\ g : NN -onto-> X ) -> g Fn NN )
8 nnex 
 |-  NN e. _V
9 8 a1i 
 |-  ( ( ph /\ g : NN -onto-> X ) -> NN e. _V )
10 ltwenn 
 |-  < We NN
11 10 a1i 
 |-  ( ( ph /\ g : NN -onto-> X ) -> < We NN )
12 7 9 11 wessf1orn 
 |-  ( ( ph /\ g : NN -onto-> X ) -> E. x e. ~P NN ( g |` x ) : x -1-1-onto-> ran g )
13 elpwi 
 |-  ( x e. ~P NN -> x C_ NN )
14 13 3ad2ant2 
 |-  ( ( ( ph /\ g : NN -onto-> X ) /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> x C_ NN )
15 simpr 
 |-  ( ( g : NN -onto-> X /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : x -1-1-onto-> ran g )
16 forn 
 |-  ( g : NN -onto-> X -> ran g = X )
17 16 adantr 
 |-  ( ( g : NN -onto-> X /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ran g = X )
18 17 f1oeq3d 
 |-  ( ( g : NN -onto-> X /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( ( g |` x ) : x -1-1-onto-> ran g <-> ( g |` x ) : x -1-1-onto-> X ) )
19 15 18 mpbid 
 |-  ( ( g : NN -onto-> X /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : x -1-1-onto-> X )
20 19 adantll 
 |-  ( ( ( ph /\ g : NN -onto-> X ) /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : x -1-1-onto-> X )
21 20 3adant2 
 |-  ( ( ( ph /\ g : NN -onto-> X ) /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> ( g |` x ) : x -1-1-onto-> X )
22 3 adantr 
 |-  ( ( ph /\ g : NN -onto-> X ) -> Disj_ y e. X y )
23 22 3ad2ant1 
 |-  ( ( ( ph /\ g : NN -onto-> X ) /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> Disj_ y e. X y )
24 eqeq1 
 |-  ( m = n -> ( m = 1 <-> n = 1 ) )
25 oveq1 
 |-  ( m = n -> ( m - 1 ) = ( n - 1 ) )
26 25 eleq1d 
 |-  ( m = n -> ( ( m - 1 ) e. x <-> ( n - 1 ) e. x ) )
27 26 notbid 
 |-  ( m = n -> ( -. ( m - 1 ) e. x <-> -. ( n - 1 ) e. x ) )
28 24 27 orbi12d 
 |-  ( m = n -> ( ( m = 1 \/ -. ( m - 1 ) e. x ) <-> ( n = 1 \/ -. ( n - 1 ) e. x ) ) )
29 fvoveq1 
 |-  ( m = n -> ( ( g |` x ) ` ( m - 1 ) ) = ( ( g |` x ) ` ( n - 1 ) ) )
30 28 29 ifbieq2d 
 |-  ( m = n -> if ( ( m = 1 \/ -. ( m - 1 ) e. x ) , (/) , ( ( g |` x ) ` ( m - 1 ) ) ) = if ( ( n = 1 \/ -. ( n - 1 ) e. x ) , (/) , ( ( g |` x ) ` ( n - 1 ) ) ) )
31 30 cbvmptv 
 |-  ( m e. NN |-> if ( ( m = 1 \/ -. ( m - 1 ) e. x ) , (/) , ( ( g |` x ) ` ( m - 1 ) ) ) ) = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. x ) , (/) , ( ( g |` x ) ` ( n - 1 ) ) ) )
32 14 21 23 31 nnfoctbdjlem 
 |-  ( ( ( ph /\ g : NN -onto-> X ) /\ x e. ~P NN /\ ( g |` x ) : x -1-1-onto-> ran g ) -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) )
33 32 3exp 
 |-  ( ( ph /\ g : NN -onto-> X ) -> ( x e. ~P NN -> ( ( g |` x ) : x -1-1-onto-> ran g -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) ) ) )
34 33 rexlimdv 
 |-  ( ( ph /\ g : NN -onto-> X ) -> ( E. x e. ~P NN ( g |` x ) : x -1-1-onto-> ran g -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) ) )
35 12 34 mpd 
 |-  ( ( ph /\ g : NN -onto-> X ) -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) )
36 35 ex 
 |-  ( ph -> ( g : NN -onto-> X -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) ) )
37 36 exlimdv 
 |-  ( ph -> ( E. g g : NN -onto-> X -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) ) )
38 5 37 mpd 
 |-  ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) )