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

Theorem cfflb 9669
Description: If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 9668 motivate the picture of (cf‘𝐴) as the greatest lower bound of the domain of cofinal maps into 𝐴. (Contributed by Mario Carneiro, 28-Feb-2013.)
Assertion
Ref Expression
cfflb ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → (cf‘𝐴) ⊆ 𝐵))
Distinct variable groups:   𝐴,𝑓,𝑤,𝑧   𝐵,𝑓,𝑤,𝑧

Proof of Theorem cfflb
Dummy variables 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frn 6513 . . . . . . 7 (𝑓:𝐵𝐴 → ran 𝑓𝐴)
21adantr 481 . . . . . 6 ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → ran 𝑓𝐴)
3 ffn 6507 . . . . . . . . . . 11 (𝑓:𝐵𝐴𝑓 Fn 𝐵)
4 fnfvelrn 6840 . . . . . . . . . . 11 ((𝑓 Fn 𝐵𝑤𝐵) → (𝑓𝑤) ∈ ran 𝑓)
53, 4sylan 580 . . . . . . . . . 10 ((𝑓:𝐵𝐴𝑤𝐵) → (𝑓𝑤) ∈ ran 𝑓)
6 sseq2 3990 . . . . . . . . . . 11 (𝑠 = (𝑓𝑤) → (𝑧𝑠𝑧 ⊆ (𝑓𝑤)))
76rspcev 3620 . . . . . . . . . 10 (((𝑓𝑤) ∈ ran 𝑓𝑧 ⊆ (𝑓𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧𝑠)
85, 7sylan 580 . . . . . . . . 9 (((𝑓:𝐵𝐴𝑤𝐵) ∧ 𝑧 ⊆ (𝑓𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧𝑠)
98rexlimdva2 3284 . . . . . . . 8 (𝑓:𝐵𝐴 → (∃𝑤𝐵 𝑧 ⊆ (𝑓𝑤) → ∃𝑠 ∈ ran 𝑓 𝑧𝑠))
109ralimdv 3175 . . . . . . 7 (𝑓:𝐵𝐴 → (∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤) → ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))
1110imp 407 . . . . . 6 ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)
122, 11jca 512 . . . . 5 ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))
13 fvex 6676 . . . . . 6 (card‘ran 𝑓) ∈ V
14 cfval 9657 . . . . . . . . . . 11 (𝐴 ∈ On → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
1514adantr 481 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
16153ad2ant2 1126 . . . . . . . . 9 ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
17 vex 3495 . . . . . . . . . . . . . 14 𝑓 ∈ V
1817rnex 7606 . . . . . . . . . . . . 13 ran 𝑓 ∈ V
19 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑦 = ran 𝑓 → (card‘𝑦) = (card‘ran 𝑓))
2019eqeq2d 2829 . . . . . . . . . . . . . 14 (𝑦 = ran 𝑓 → (𝑥 = (card‘𝑦) ↔ 𝑥 = (card‘ran 𝑓)))
21 sseq1 3989 . . . . . . . . . . . . . . 15 (𝑦 = ran 𝑓 → (𝑦𝐴 ↔ ran 𝑓𝐴))
22 rexeq 3404 . . . . . . . . . . . . . . . 16 (𝑦 = ran 𝑓 → (∃𝑠𝑦 𝑧𝑠 ↔ ∃𝑠 ∈ ran 𝑓 𝑧𝑠))
2322ralbidv 3194 . . . . . . . . . . . . . . 15 (𝑦 = ran 𝑓 → (∀𝑧𝐴𝑠𝑦 𝑧𝑠 ↔ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))
2421, 23anbi12d 630 . . . . . . . . . . . . . 14 (𝑦 = ran 𝑓 → ((𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠) ↔ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)))
2520, 24anbi12d 630 . . . . . . . . . . . . 13 (𝑦 = ran 𝑓 → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠)) ↔ (𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))))
2618, 25spcev 3604 . . . . . . . . . . . 12 ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠)))
27 abid 2800 . . . . . . . . . . . 12 (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ↔ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠)))
2826, 27sylibr 235 . . . . . . . . . . 11 ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → 𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
29 intss1 4882 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ⊆ 𝑥)
3028, 29syl 17 . . . . . . . . . 10 ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ⊆ 𝑥)
31303adant2 1123 . . . . . . . . 9 ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ⊆ 𝑥)
3216, 31eqsstrd 4002 . . . . . . . 8 ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ 𝑥)
33323expib 1114 . . . . . . 7 (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ 𝑥))
34 sseq2 3990 . . . . . . 7 (𝑥 = (card‘ran 𝑓) → ((cf‘𝐴) ⊆ 𝑥 ↔ (cf‘𝐴) ⊆ (card‘ran 𝑓)))
3533, 34sylibd 240 . . . . . 6 (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓)))
3613, 35vtocle 3581 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓))
3712, 36sylan2 592 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤))) → (cf‘𝐴) ⊆ (card‘ran 𝑓))
38 cardidm 9376 . . . . . . 7 (card‘(card‘ran 𝑓)) = (card‘ran 𝑓)
39 onss 7494 . . . . . . . . . . . . . 14 (𝐴 ∈ On → 𝐴 ⊆ On)
401, 39sylan9ssr 3978 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓 ⊆ On)
41403adant2 1123 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓 ⊆ On)
42 onssnum 9454 . . . . . . . . . . . 12 ((ran 𝑓 ∈ V ∧ ran 𝑓 ⊆ On) → ran 𝑓 ∈ dom card)
4318, 41, 42sylancr 587 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓 ∈ dom card)
44 cardid2 9370 . . . . . . . . . . 11 (ran 𝑓 ∈ dom card → (card‘ran 𝑓) ≈ ran 𝑓)
4543, 44syl 17 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ≈ ran 𝑓)
46 onenon 9366 . . . . . . . . . . . . 13 (𝐵 ∈ On → 𝐵 ∈ dom card)
47 dffn4 6589 . . . . . . . . . . . . . 14 (𝑓 Fn 𝐵𝑓:𝐵onto→ran 𝑓)
483, 47sylib 219 . . . . . . . . . . . . 13 (𝑓:𝐵𝐴𝑓:𝐵onto→ran 𝑓)
49 fodomnum 9471 . . . . . . . . . . . . 13 (𝐵 ∈ dom card → (𝑓:𝐵onto→ran 𝑓 → ran 𝑓𝐵))
5046, 48, 49syl2im 40 . . . . . . . . . . . 12 (𝐵 ∈ On → (𝑓:𝐵𝐴 → ran 𝑓𝐵))
5150imp 407 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓𝐵)
52513adant1 1122 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓𝐵)
53 endomtr 8555 . . . . . . . . . 10 (((card‘ran 𝑓) ≈ ran 𝑓 ∧ ran 𝑓𝐵) → (card‘ran 𝑓) ≼ 𝐵)
5445, 52, 53syl2anc 584 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ≼ 𝐵)
55 cardon 9361 . . . . . . . . . . . 12 (card‘ran 𝑓) ∈ On
56 onenon 9366 . . . . . . . . . . . 12 ((card‘ran 𝑓) ∈ On → (card‘ran 𝑓) ∈ dom card)
5755, 56ax-mp 5 . . . . . . . . . . 11 (card‘ran 𝑓) ∈ dom card
58 carddom2 9394 . . . . . . . . . . 11 (((card‘ran 𝑓) ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵))
5957, 46, 58sylancr 587 . . . . . . . . . 10 (𝐵 ∈ On → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵))
60593ad2ant2 1126 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵))
6154, 60mpbird 258 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘(card‘ran 𝑓)) ⊆ (card‘𝐵))
62 cardonle 9374 . . . . . . . . 9 (𝐵 ∈ On → (card‘𝐵) ⊆ 𝐵)
63623ad2ant2 1126 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘𝐵) ⊆ 𝐵)
6461, 63sstrd 3974 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘(card‘ran 𝑓)) ⊆ 𝐵)
6538, 64eqsstrrid 4013 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ⊆ 𝐵)
66653expa 1110 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ⊆ 𝐵)
6766adantrr 713 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤))) → (card‘ran 𝑓) ⊆ 𝐵)
6837, 67sstrd 3974 . . 3 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤))) → (cf‘𝐴) ⊆ 𝐵)
6968ex 413 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → (cf‘𝐴) ⊆ 𝐵))
7069exlimdv 1925 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → (cf‘𝐴) ⊆ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wral 3135  wrex 3136  Vcvv 3492  wss 3933   cint 4867   class class class wbr 5057  dom cdm 5548  ran crn 5549  Oncon0 6184   Fn wfn 6343  wf 6344  ontowfo 6346  cfv 6348  cen 8494  cdom 8495  cardccrd 9352  cfccf 9354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-card 9356  df-cf 9358  df-acn 9359
This theorem is referenced by:  cfsmolem  9680  cfcoflem  9682  cfcof  9684  inar1  10185
  Copyright terms: Public domain W3C validator