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

Theorem cfslb 9673
 Description: Any cofinal subset of 𝐴 is at least as large as (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.)
Hypothesis
Ref Expression
cfslb.1 𝐴 ∈ V
Assertion
Ref Expression
cfslb ((Lim 𝐴𝐵𝐴 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵)

Proof of Theorem cfslb
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fvex 6664 . . 3 (card‘𝐵) ∈ V
2 ssid 3973 . . . . . . 7 (card‘𝐵) ⊆ (card‘𝐵)
3 cfslb.1 . . . . . . . . . . 11 𝐴 ∈ V
43ssex 5206 . . . . . . . . . 10 (𝐵𝐴𝐵 ∈ V)
54ad2antrr 725 . . . . . . . . 9 (((𝐵𝐴 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → 𝐵 ∈ V)
6 velpw 4525 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
7 sseq1 3976 . . . . . . . . . . . . 13 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
86, 7syl5bb 286 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝑥 ∈ 𝒫 𝐴𝐵𝐴))
9 unieq 4830 . . . . . . . . . . . . 13 (𝑥 = 𝐵 𝑥 = 𝐵)
109eqeq1d 2826 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ( 𝑥 = 𝐴 𝐵 = 𝐴))
118, 10anbi12d 633 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ↔ (𝐵𝐴 𝐵 = 𝐴)))
12 fveq2 6651 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (card‘𝑥) = (card‘𝐵))
1312sseq1d 3982 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((card‘𝑥) ⊆ (card‘𝐵) ↔ (card‘𝐵) ⊆ (card‘𝐵)))
1411, 13anbi12d 633 . . . . . . . . . 10 (𝑥 = 𝐵 → (((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ((𝐵𝐴 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵))))
1514spcegv 3582 . . . . . . . . 9 (𝐵 ∈ V → (((𝐵𝐴 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵))))
165, 15mpcom 38 . . . . . . . 8 (((𝐵𝐴 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)))
17 df-rex 3138 . . . . . . . . 9 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)))
18 rabid 3369 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴))
1918anbi1i 626 . . . . . . . . . 10 ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)))
2019exbii 1849 . . . . . . . . 9 (∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} ∧ (card‘𝑥) ⊆ (card‘𝐵)) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)))
2117, 20bitri 278 . . . . . . . 8 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴) ∧ (card‘𝑥) ⊆ (card‘𝐵)))
2216, 21sylibr 237 . . . . . . 7 (((𝐵𝐴 𝐵 = 𝐴) ∧ (card‘𝐵) ⊆ (card‘𝐵)) → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵))
232, 22mpan2 690 . . . . . 6 ((𝐵𝐴 𝐵 = 𝐴) → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵))
24 iinss 4961 . . . . . 6 (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵))
2523, 24syl 17 . . . . 5 ((𝐵𝐴 𝐵 = 𝐴) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵))
263cflim3 9669 . . . . . 6 (Lim 𝐴 → (cf‘𝐴) = 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥))
2726sseq1d 3982 . . . . 5 (Lim 𝐴 → ((cf‘𝐴) ⊆ (card‘𝐵) ↔ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴} (card‘𝑥) ⊆ (card‘𝐵)))
2825, 27syl5ibr 249 . . . 4 (Lim 𝐴 → ((𝐵𝐴 𝐵 = 𝐴) → (cf‘𝐴) ⊆ (card‘𝐵)))
29283impib 1113 . . 3 ((Lim 𝐴𝐵𝐴 𝐵 = 𝐴) → (cf‘𝐴) ⊆ (card‘𝐵))
30 ssdomg 8538 . . 3 ((card‘𝐵) ∈ V → ((cf‘𝐴) ⊆ (card‘𝐵) → (cf‘𝐴) ≼ (card‘𝐵)))
311, 29, 30mpsyl 68 . 2 ((Lim 𝐴𝐵𝐴 𝐵 = 𝐴) → (cf‘𝐴) ≼ (card‘𝐵))
32 limord 6231 . . . . . . 7 (Lim 𝐴 → Ord 𝐴)
33 ordsson 7487 . . . . . . 7 (Ord 𝐴𝐴 ⊆ On)
3432, 33syl 17 . . . . . 6 (Lim 𝐴𝐴 ⊆ On)
35 sstr2 3958 . . . . . 6 (𝐵𝐴 → (𝐴 ⊆ On → 𝐵 ⊆ On))
3634, 35mpan9 510 . . . . 5 ((Lim 𝐴𝐵𝐴) → 𝐵 ⊆ On)
37 onssnum 9451 . . . . 5 ((𝐵 ∈ V ∧ 𝐵 ⊆ On) → 𝐵 ∈ dom card)
384, 36, 37syl2an2 685 . . . 4 ((Lim 𝐴𝐵𝐴) → 𝐵 ∈ dom card)
39 cardid2 9366 . . . 4 (𝐵 ∈ dom card → (card‘𝐵) ≈ 𝐵)
4038, 39syl 17 . . 3 ((Lim 𝐴𝐵𝐴) → (card‘𝐵) ≈ 𝐵)
41403adant3 1129 . 2 ((Lim 𝐴𝐵𝐴 𝐵 = 𝐴) → (card‘𝐵) ≈ 𝐵)
42 domentr 8551 . 2 (((cf‘𝐴) ≼ (card‘𝐵) ∧ (card‘𝐵) ≈ 𝐵) → (cf‘𝐴) ≼ 𝐵)
4331, 41, 42syl2anc 587 1 ((Lim 𝐴𝐵𝐴 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115  ∃wrex 3133  {crab 3136  Vcvv 3479   ⊆ wss 3918  𝒫 cpw 4520  ∪ cuni 4819  ∩ ciin 4901   class class class wbr 5047  dom cdm 5536  Ord word 6171  Oncon0 6172  Lim wlim 6173  ‘cfv 6336   ≈ cen 8489   ≼ cdom 8490  cardccrd 9348  cfccf 9350 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-int 4858  df-iun 4902  df-iin 4903  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-se 5496  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7096  df-wrecs 7930  df-recs 7991  df-er 8272  df-en 8493  df-dom 8494  df-card 9352  df-cf 9354 This theorem is referenced by:  cfslbn  9674  cfslb2n  9675  rankcf  10184
 Copyright terms: Public domain W3C validator