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 ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω ) )

Proof

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