Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cfss Structured version   Visualization version   GIF version

Theorem cfss 9125
 Description: There is a cofinal subset of 𝐴 of cardinality (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.)
Hypothesis
Ref Expression
cfss.1 𝐴 ∈ V
Assertion
Ref Expression
cfss (Lim 𝐴 → ∃𝑥(𝑥𝐴𝑥 ≈ (cf‘𝐴) ∧ 𝑥 = 𝐴))
Distinct variable group:   𝑥,𝐴

Proof of Theorem cfss
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cfss.1 . . . . . 6 𝐴 ∈ V
21cflim3 9122 . . . . 5 (Lim 𝐴 → (cf‘𝐴) = 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥))
3 fvex 6239 . . . . . . 7 (card‘𝑥) ∈ V
43dfiin2 4587 . . . . . 6 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) = {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)}
5 cardon 8808 . . . . . . . . . 10 (card‘𝑥) ∈ On
6 eleq1 2718 . . . . . . . . . 10 (𝑦 = (card‘𝑥) → (𝑦 ∈ On ↔ (card‘𝑥) ∈ On))
75, 6mpbiri 248 . . . . . . . . 9 (𝑦 = (card‘𝑥) → 𝑦 ∈ On)
87rexlimivw 3058 . . . . . . . 8 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥) → 𝑦 ∈ On)
98abssi 3710 . . . . . . 7 {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ⊆ On
10 limuni 5823 . . . . . . . . . . . 12 (Lim 𝐴𝐴 = 𝐴)
1110eqcomd 2657 . . . . . . . . . . 11 (Lim 𝐴 𝐴 = 𝐴)
12 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → (card‘𝑥) = (card‘𝐴))
1312eqcomd 2657 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (card‘𝐴) = (card‘𝑥))
1413biantrud 527 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ( 𝐴 = 𝐴 ↔ ( 𝐴 = 𝐴 ∧ (card‘𝐴) = (card‘𝑥))))
15 unieq 4476 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 𝑥 = 𝐴)
1615eqeq1d 2653 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → ( 𝑥 = 𝐴 𝐴 = 𝐴))
171pwid 4207 . . . . . . . . . . . . . . . . 17 𝐴 ∈ 𝒫 𝐴
18 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐴 → (𝑥 ∈ 𝒫 𝐴𝐴 ∈ 𝒫 𝐴))
1917, 18mpbiri 248 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴𝑥 ∈ 𝒫 𝐴)
2019biantrurd 528 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → ( 𝑥 = 𝐴 ↔ (𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴)))
2116, 20bitr3d 270 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → ( 𝐴 = 𝐴 ↔ (𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴)))
2221anbi1d 741 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → (( 𝐴 = 𝐴 ∧ (card‘𝐴) = (card‘𝑥)) ↔ ((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥))))
2314, 22bitr2d 269 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)) ↔ 𝐴 = 𝐴))
241, 23spcev 3331 . . . . . . . . . . 11 ( 𝐴 = 𝐴 → ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)))
2511, 24syl 17 . . . . . . . . . 10 (Lim 𝐴 → ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)))
26 df-rex 2947 . . . . . . . . . . 11 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (card‘𝐴) = (card‘𝑥)))
27 rabid 3145 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴))
2827anbi1i 731 . . . . . . . . . . . 12 ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (card‘𝐴) = (card‘𝑥)) ↔ ((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)))
2928exbii 1814 . . . . . . . . . . 11 (∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (card‘𝐴) = (card‘𝑥)) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)))
3026, 29bitri 264 . . . . . . . . . 10 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)))
3125, 30sylibr 224 . . . . . . . . 9 (Lim 𝐴 → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥))
32 fvex 6239 . . . . . . . . . 10 (card‘𝐴) ∈ V
33 eqeq1 2655 . . . . . . . . . . 11 (𝑦 = (card‘𝐴) → (𝑦 = (card‘𝑥) ↔ (card‘𝐴) = (card‘𝑥)))
3433rexbidv 3081 . . . . . . . . . 10 (𝑦 = (card‘𝐴) → (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥)))
3532, 34spcev 3331 . . . . . . . . 9 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥) → ∃𝑦𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥))
3631, 35syl 17 . . . . . . . 8 (Lim 𝐴 → ∃𝑦𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥))
37 abn0 3987 . . . . . . . 8 ({𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ≠ ∅ ↔ ∃𝑦𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥))
3836, 37sylibr 224 . . . . . . 7 (Lim 𝐴 → {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ≠ ∅)
39 onint 7037 . . . . . . 7 (({𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ⊆ On ∧ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ≠ ∅) → {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)})
409, 38, 39sylancr 696 . . . . . 6 (Lim 𝐴 {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)})
414, 40syl5eqel 2734 . . . . 5 (Lim 𝐴 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)})
422, 41eqeltrd 2730 . . . 4 (Lim 𝐴 → (cf‘𝐴) ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)})
43 fvex 6239 . . . . 5 (cf‘𝐴) ∈ V
44 eqeq1 2655 . . . . . 6 (𝑦 = (cf‘𝐴) → (𝑦 = (card‘𝑥) ↔ (cf‘𝐴) = (card‘𝑥)))
4544rexbidv 3081 . . . . 5 (𝑦 = (cf‘𝐴) → (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥)))
4643, 45elab 3382 . . . 4 ((cf‘𝐴) ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ↔ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥))
4742, 46sylib 208 . . 3 (Lim 𝐴 → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥))
48 df-rex 2947 . . 3 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥)))
4947, 48sylib 208 . 2 (Lim 𝐴 → ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥)))
50 simprl 809 . . . . . . . 8 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴})
5150, 27sylib 208 . . . . . . 7 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → (𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴))
5251simpld 474 . . . . . 6 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ∈ 𝒫 𝐴)
5352elpwid 4203 . . . . 5 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥𝐴)
54 simpl 472 . . . . . . 7 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → Lim 𝐴)
55 vex 3234 . . . . . . . . . 10 𝑥 ∈ V
56 limord 5822 . . . . . . . . . . . 12 (Lim 𝐴 → Ord 𝐴)
57 ordsson 7031 . . . . . . . . . . . 12 (Ord 𝐴𝐴 ⊆ On)
5856, 57syl 17 . . . . . . . . . . 11 (Lim 𝐴𝐴 ⊆ On)
59 sstr 3644 . . . . . . . . . . 11 ((𝑥𝐴𝐴 ⊆ On) → 𝑥 ⊆ On)
6058, 59sylan2 490 . . . . . . . . . 10 ((𝑥𝐴 ∧ Lim 𝐴) → 𝑥 ⊆ On)
61 onssnum 8901 . . . . . . . . . 10 ((𝑥 ∈ V ∧ 𝑥 ⊆ On) → 𝑥 ∈ dom card)
6255, 60, 61sylancr 696 . . . . . . . . 9 ((𝑥𝐴 ∧ Lim 𝐴) → 𝑥 ∈ dom card)
63 cardid2 8817 . . . . . . . . 9 (𝑥 ∈ dom card → (card‘𝑥) ≈ 𝑥)
6462, 63syl 17 . . . . . . . 8 ((𝑥𝐴 ∧ Lim 𝐴) → (card‘𝑥) ≈ 𝑥)
6564ensymd 8048 . . . . . . 7 ((𝑥𝐴 ∧ Lim 𝐴) → 𝑥 ≈ (card‘𝑥))
6653, 54, 65syl2anc 694 . . . . . 6 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ≈ (card‘𝑥))
67 simprr 811 . . . . . 6 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → (cf‘𝐴) = (card‘𝑥))
6866, 67breqtrrd 4713 . . . . 5 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ≈ (cf‘𝐴))
6951simprd 478 . . . . 5 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 = 𝐴)
7053, 68, 693jca 1261 . . . 4 ((Lim 𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → (𝑥𝐴𝑥 ≈ (cf‘𝐴) ∧ 𝑥 = 𝐴))
7170ex 449 . . 3 (Lim 𝐴 → ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥)) → (𝑥𝐴𝑥 ≈ (cf‘𝐴) ∧ 𝑥 = 𝐴)))
7271eximdv 1886 . 2 (Lim 𝐴 → (∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥)) → ∃𝑥(𝑥𝐴𝑥 ≈ (cf‘𝐴) ∧ 𝑥 = 𝐴)))
7349, 72mpd 15 1 (Lim 𝐴 → ∃𝑥(𝑥𝐴𝑥 ≈ (cf‘𝐴) ∧ 𝑥 = 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ∃wex 1744   ∈ wcel 2030  {cab 2637   ≠ wne 2823  ∃wrex 2942  {crab 2945  Vcvv 3231   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191  ∪ cuni 4468  ∩ cint 4507  ∩ ciin 4553   class class class wbr 4685  dom cdm 5143  Ord word 5760  Oncon0 5761  Lim wlim 5762  ‘cfv 5926   ≈ cen 7994  cardccrd 8799  cfccf 8801 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-wrecs 7452  df-recs 7513  df-er 7787  df-en 7998  df-dom 7999  df-card 8803  df-cf 8805 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator