Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ctbssinf Structured version   Visualization version   GIF version

Theorem ctbssinf 34237
Description: Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020.)
Assertion
Ref Expression
ctbssinf 𝐴 ∈ Fin → ∃𝑥(𝑥𝐴𝑥 ≈ ω))
Distinct variable group:   𝑥,𝐴

Proof of Theorem ctbssinf
Dummy variables 𝑓 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isinf 8577 . 2 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥𝐴𝑥𝑛))
2 omex 8952 . . 3 ω ∈ V
3 sseq1 3913 . . . 4 (𝑥 = (𝑓𝑛) → (𝑥𝐴 ↔ (𝑓𝑛) ⊆ 𝐴))
4 breq1 4965 . . . 4 (𝑥 = (𝑓𝑛) → (𝑥𝑛 ↔ (𝑓𝑛) ≈ 𝑛))
53, 4anbi12d 630 . . 3 (𝑥 = (𝑓𝑛) → ((𝑥𝐴𝑥𝑛) ↔ ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)))
62, 5ac6s2 9754 . 2 (∀𝑛 ∈ ω ∃𝑥(𝑥𝐴𝑥𝑛) → ∃𝑓(𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)))
7 simpl 483 . . . . . 6 (((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → (𝑓𝑛) ⊆ 𝐴)
87ralimi 3127 . . . . 5 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω (𝑓𝑛) ⊆ 𝐴)
9 fvex 6551 . . . . . . . 8 (𝑓𝑛) ∈ V
109elpw 4459 . . . . . . 7 ((𝑓𝑛) ∈ 𝒫 𝐴 ↔ (𝑓𝑛) ⊆ 𝐴)
1110ralbii 3132 . . . . . 6 (∀𝑛 ∈ ω (𝑓𝑛) ∈ 𝒫 𝐴 ↔ ∀𝑛 ∈ ω (𝑓𝑛) ⊆ 𝐴)
12 fnfvrnss 6747 . . . . . . 7 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω (𝑓𝑛) ∈ 𝒫 𝐴) → ran 𝑓 ⊆ 𝒫 𝐴)
13 uniss 4766 . . . . . . . 8 (ran 𝑓 ⊆ 𝒫 𝐴 ran 𝑓 𝒫 𝐴)
14 unipw 5234 . . . . . . . 8 𝒫 𝐴 = 𝐴
1513, 14syl6sseq 3938 . . . . . . 7 (ran 𝑓 ⊆ 𝒫 𝐴 ran 𝑓𝐴)
1612, 15syl 17 . . . . . 6 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω (𝑓𝑛) ∈ 𝒫 𝐴) → ran 𝑓𝐴)
1711, 16sylan2br 594 . . . . 5 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω (𝑓𝑛) ⊆ 𝐴) → ran 𝑓𝐴)
188, 17sylan2 592 . . . 4 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ran 𝑓𝐴)
19 dffn5 6592 . . . . . . . . . . 11 (𝑓 Fn ω ↔ 𝑓 = (𝑛 ∈ ω ↦ (𝑓𝑛)))
2019biimpi 217 . . . . . . . . . 10 (𝑓 Fn ω → 𝑓 = (𝑛 ∈ ω ↦ (𝑓𝑛)))
2120rneqd 5690 . . . . . . . . 9 (𝑓 Fn ω → ran 𝑓 = ran (𝑛 ∈ ω ↦ (𝑓𝑛)))
2221unieqd 4755 . . . . . . . 8 (𝑓 Fn ω → ran 𝑓 = ran (𝑛 ∈ ω ↦ (𝑓𝑛)))
239dfiun3 5718 . . . . . . . 8 𝑛 ∈ ω (𝑓𝑛) = ran (𝑛 ∈ ω ↦ (𝑓𝑛))
2422, 23syl6eqr 2849 . . . . . . 7 (𝑓 Fn ω → ran 𝑓 = 𝑛 ∈ ω (𝑓𝑛))
2524adantr 481 . . . . . 6 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ran 𝑓 = 𝑛 ∈ ω (𝑓𝑛))
26 simpr 485 . . . . . . . . 9 (((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → (𝑓𝑛) ≈ 𝑛)
2726ralimi 3127 . . . . . . . 8 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω (𝑓𝑛) ≈ 𝑛)
28 endom 8384 . . . . . . . . . 10 ((𝑓𝑛) ≈ 𝑛 → (𝑓𝑛) ≼ 𝑛)
29 nnsdom 8963 . . . . . . . . . 10 (𝑛 ∈ ω → 𝑛 ≺ ω)
30 domsdomtr 8499 . . . . . . . . . . 11 (((𝑓𝑛) ≼ 𝑛𝑛 ≺ ω) → (𝑓𝑛) ≺ ω)
31 sdomdom 8385 . . . . . . . . . . 11 ((𝑓𝑛) ≺ ω → (𝑓𝑛) ≼ ω)
3230, 31syl 17 . . . . . . . . . 10 (((𝑓𝑛) ≼ 𝑛𝑛 ≺ ω) → (𝑓𝑛) ≼ ω)
3328, 29, 32syl2anr 596 . . . . . . . . 9 ((𝑛 ∈ ω ∧ (𝑓𝑛) ≈ 𝑛) → (𝑓𝑛) ≼ ω)
3433ralimiaa 3126 . . . . . . . 8 (∀𝑛 ∈ ω (𝑓𝑛) ≈ 𝑛 → ∀𝑛 ∈ ω (𝑓𝑛) ≼ ω)
35 iunctb2 34234 . . . . . . . 8 (∀𝑛 ∈ ω (𝑓𝑛) ≼ ω → 𝑛 ∈ ω (𝑓𝑛) ≼ ω)
3627, 34, 353syl 18 . . . . . . 7 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → 𝑛 ∈ ω (𝑓𝑛) ≼ ω)
3736adantl 482 . . . . . 6 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → 𝑛 ∈ ω (𝑓𝑛) ≼ ω)
3825, 37eqbrtrd 4984 . . . . 5 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ran 𝑓 ≼ ω)
39 fvssunirn 6567 . . . . . . . . . 10 (𝑓𝑛) ⊆ ran 𝑓
4039jctl 524 . . . . . . . . 9 ((𝑓𝑛) ≈ 𝑛 → ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛))
4140adantl 482 . . . . . . . 8 (((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛))
4241ralimi 3127 . . . . . . 7 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛))
43 sseq1 3913 . . . . . . . . . . . 12 (𝑥 = (𝑓𝑛) → (𝑥 ran 𝑓 ↔ (𝑓𝑛) ⊆ ran 𝑓))
4443, 4anbi12d 630 . . . . . . . . . . 11 (𝑥 = (𝑓𝑛) → ((𝑥 ran 𝑓𝑥𝑛) ↔ ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛)))
459, 44spcev 3549 . . . . . . . . . 10 (((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛) → ∃𝑥(𝑥 ran 𝑓𝑥𝑛))
4645ralimi 3127 . . . . . . . . 9 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛) → ∀𝑛 ∈ ω ∃𝑥(𝑥 ran 𝑓𝑥𝑛))
47 isinf2 34236 . . . . . . . . 9 (∀𝑛 ∈ ω ∃𝑥(𝑥 ran 𝑓𝑥𝑛) → ¬ ran 𝑓 ∈ Fin)
4846, 47syl 17 . . . . . . . 8 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛) → ¬ ran 𝑓 ∈ Fin)
49 vex 3440 . . . . . . . . . . 11 𝑓 ∈ V
5049rnex 7473 . . . . . . . . . 10 ran 𝑓 ∈ V
5150uniex 7323 . . . . . . . . 9 ran 𝑓 ∈ V
52 infinf 9834 . . . . . . . . 9 ( ran 𝑓 ∈ V → (¬ ran 𝑓 ∈ Fin ↔ ω ≼ ran 𝑓))
5351, 52ax-mp 5 . . . . . . . 8 ran 𝑓 ∈ Fin ↔ ω ≼ ran 𝑓)
5448, 53sylib 219 . . . . . . 7 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ ran 𝑓 ∧ (𝑓𝑛) ≈ 𝑛) → ω ≼ ran 𝑓)
5542, 54syl 17 . . . . . 6 (∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛) → ω ≼ ran 𝑓)
5655adantl 482 . . . . 5 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ω ≼ ran 𝑓)
57 sbth 8484 . . . . 5 (( ran 𝑓 ≼ ω ∧ ω ≼ ran 𝑓) → ran 𝑓 ≈ ω)
5838, 56, 57syl2anc 584 . . . 4 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ran 𝑓 ≈ ω)
59 sseq1 3913 . . . . . 6 (𝑥 = ran 𝑓 → (𝑥𝐴 ran 𝑓𝐴))
60 breq1 4965 . . . . . 6 (𝑥 = ran 𝑓 → (𝑥 ≈ ω ↔ ran 𝑓 ≈ ω))
6159, 60anbi12d 630 . . . . 5 (𝑥 = ran 𝑓 → ((𝑥𝐴𝑥 ≈ ω) ↔ ( ran 𝑓𝐴 ran 𝑓 ≈ ω)))
6251, 61spcev 3549 . . . 4 (( ran 𝑓𝐴 ran 𝑓 ≈ ω) → ∃𝑥(𝑥𝐴𝑥 ≈ ω))
6318, 58, 62syl2anc 584 . . 3 ((𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ∃𝑥(𝑥𝐴𝑥 ≈ ω))
6463exlimiv 1908 . 2 (∃𝑓(𝑓 Fn ω ∧ ∀𝑛 ∈ ω ((𝑓𝑛) ⊆ 𝐴 ∧ (𝑓𝑛) ≈ 𝑛)) → ∃𝑥(𝑥𝐴𝑥 ≈ ω))
651, 6, 643syl 18 1 𝐴 ∈ Fin → ∃𝑥(𝑥𝐴𝑥 ≈ ω))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1522  wex 1761  wcel 2081  wral 3105  Vcvv 3437  wss 3859  𝒫 cpw 4453   cuni 4745   ciun 4825   class class class wbr 4962  cmpt 5041  ran crn 5444   Fn wfn 6220  cfv 6225  ωcom 7436  cen 8354  cdom 8355  csdm 8356  Fincfn 8357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-reg 8902  ax-inf2 8950  ax-cc 9703  ax-ac2 9731
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-oi 8820  df-r1 9039  df-rank 9040  df-card 9214  df-acn 9217  df-ac 9388
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator