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 Fin x x A x ω

Proof

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