Metamath Proof Explorer

Theorem ctbssinf

Description: Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020)

Ref Expression
Assertion ctbssinf 
|- ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ _om ) )

Proof

Step Hyp Ref Expression
1 isinf 
 |-  ( -. A e. Fin -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )
2 omex 
 |-  _om e. _V
3 sseq1 
 |-  ( x = ( f ` n ) -> ( x C_ A <-> ( f ` n ) C_ A ) )
4 breq1 
 |-  ( x = ( f ` n ) -> ( x ~~ n <-> ( f ` n ) ~~ n ) )
5 3 4 anbi12d 
 |-  ( x = ( f ` n ) -> ( ( x C_ A /\ x ~~ n ) <-> ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) )
6 2 5 ac6s2 
 |-  ( A. n e. _om E. x ( x C_ A /\ x ~~ n ) -> E. f ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) )
7 simpl 
 |-  ( ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> ( f ` n ) C_ A )
8 7 ralimi 
 |-  ( A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> A. n e. _om ( f ` n ) C_ A )
9 fvex 
 |-  ( f ` n ) e. _V
10 9 elpw 
 |-  ( ( f ` n ) e. ~P A <-> ( f ` n ) C_ A )
11 10 ralbii 
 |-  ( A. n e. _om ( f ` n ) e. ~P A <-> A. n e. _om ( f ` n ) C_ A )
12 fnfvrnss 
 |-  ( ( f Fn _om /\ A. n e. _om ( f ` n ) e. ~P A ) -> ran f C_ ~P A )
13 uniss 
 |-  ( ran f C_ ~P A -> U. ran f C_ U. ~P A )
14 unipw 
 |-  U. ~P A = A
15 13 14 sseqtrdi 
 |-  ( ran f C_ ~P A -> U. ran f C_ A )
16 12 15 syl 
 |-  ( ( f Fn _om /\ A. n e. _om ( f ` n ) e. ~P A ) -> U. ran f C_ A )
17 11 16 sylan2br 
 |-  ( ( f Fn _om /\ A. n e. _om ( f ` n ) C_ A ) -> U. ran f C_ A )
18 8 17 sylan2 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> U. ran f C_ A )
19 dffn5 
 |-  ( f Fn _om <-> f = ( n e. _om |-> ( f ` n ) ) )
20 19 biimpi 
 |-  ( f Fn _om -> f = ( n e. _om |-> ( f ` n ) ) )
21 20 rneqd 
 |-  ( f Fn _om -> ran f = ran ( n e. _om |-> ( f ` n ) ) )
22 21 unieqd 
 |-  ( f Fn _om -> U. ran f = U. ran ( n e. _om |-> ( f ` n ) ) )
23 9 dfiun3 
 |-  U_ n e. _om ( f ` n ) = U. ran ( n e. _om |-> ( f ` n ) )
24 22 23 eqtr4di 
 |-  ( f Fn _om -> U. ran f = U_ n e. _om ( f ` n ) )
25 24 adantr 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> U. ran f = U_ n e. _om ( f ` n ) )
26 simpr 
 |-  ( ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> ( f ` n ) ~~ n )
27 26 ralimi 
 |-  ( A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> A. n e. _om ( f ` n ) ~~ n )
28 endom 
 |-  ( ( f ` n ) ~~ n -> ( f ` n ) ~<_ n )
29 nnsdom 
 |-  ( n e. _om -> n ~< _om )
30 domsdomtr 
 |-  ( ( ( f ` n ) ~<_ n /\ n ~< _om ) -> ( f ` n ) ~< _om )
31 sdomdom 
 |-  ( ( f ` n ) ~< _om -> ( f ` n ) ~<_ _om )
32 30 31 syl 
 |-  ( ( ( f ` n ) ~<_ n /\ n ~< _om ) -> ( f ` n ) ~<_ _om )
33 28 29 32 syl2anr 
 |-  ( ( n e. _om /\ ( f ` n ) ~~ n ) -> ( f ` n ) ~<_ _om )
34 33 ralimiaa 
 |-  ( A. n e. _om ( f ` n ) ~~ n -> A. n e. _om ( f ` n ) ~<_ _om )
35 iunctb2 
 |-  ( A. n e. _om ( f ` n ) ~<_ _om -> U_ n e. _om ( f ` n ) ~<_ _om )
36 27 34 35 3syl 
 |-  ( A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> U_ n e. _om ( f ` n ) ~<_ _om )
37 36 adantl 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> U_ n e. _om ( f ` n ) ~<_ _om )
38 25 37 eqbrtrd 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> U. ran f ~<_ _om )
39 fvssunirn 
 |-  ( f ` n ) C_ U. ran f
40 39 jctl 
 |-  ( ( f ` n ) ~~ n -> ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) )
41 40 adantl 
 |-  ( ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) )
42 41 ralimi 
 |-  ( A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> A. n e. _om ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) )
43 sseq1 
 |-  ( x = ( f ` n ) -> ( x C_ U. ran f <-> ( f ` n ) C_ U. ran f ) )
44 43 4 anbi12d 
 |-  ( x = ( f ` n ) -> ( ( x C_ U. ran f /\ x ~~ n ) <-> ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) ) )
45 9 44 spcev 
 |-  ( ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) -> E. x ( x C_ U. ran f /\ x ~~ n ) )
46 45 ralimi 
 |-  ( A. n e. _om ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) -> A. n e. _om E. x ( x C_ U. ran f /\ x ~~ n ) )
47 isinf2 
 |-  ( A. n e. _om E. x ( x C_ U. ran f /\ x ~~ n ) -> -. U. ran f e. Fin )
48 46 47 syl 
 |-  ( A. n e. _om ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) -> -. U. ran f e. Fin )
49 vex 
 |-  f e. _V
50 49 rnex 
 |-  ran f e. _V
51 50 uniex 
 |-  U. ran f e. _V
52 infinf 
 |-  ( U. ran f e. _V -> ( -. U. ran f e. Fin <-> _om ~<_ U. ran f ) )
53 51 52 ax-mp 
 |-  ( -. U. ran f e. Fin <-> _om ~<_ U. ran f )
54 48 53 sylib 
 |-  ( A. n e. _om ( ( f ` n ) C_ U. ran f /\ ( f ` n ) ~~ n ) -> _om ~<_ U. ran f )
55 42 54 syl 
 |-  ( A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) -> _om ~<_ U. ran f )
56 55 adantl 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> _om ~<_ U. ran f )
57 sbth 
 |-  ( ( U. ran f ~<_ _om /\ _om ~<_ U. ran f ) -> U. ran f ~~ _om )
58 38 56 57 syl2anc 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> U. ran f ~~ _om )
59 sseq1 
 |-  ( x = U. ran f -> ( x C_ A <-> U. ran f C_ A ) )
60 breq1 
 |-  ( x = U. ran f -> ( x ~~ _om <-> U. ran f ~~ _om ) )
61 59 60 anbi12d 
 |-  ( x = U. ran f -> ( ( x C_ A /\ x ~~ _om ) <-> ( U. ran f C_ A /\ U. ran f ~~ _om ) ) )
62 51 61 spcev 
 |-  ( ( U. ran f C_ A /\ U. ran f ~~ _om ) -> E. x ( x C_ A /\ x ~~ _om ) )
63 18 58 62 syl2anc 
 |-  ( ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> E. x ( x C_ A /\ x ~~ _om ) )
64 63 exlimiv 
 |-  ( E. f ( f Fn _om /\ A. n e. _om ( ( f ` n ) C_ A /\ ( f ` n ) ~~ n ) ) -> E. x ( x C_ A /\ x ~~ _om ) )
65 1 6 64 3syl 
 |-  ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ _om ) )