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

Theorem cfflb 9670
Description: If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 9669 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 6514 . . . . . . 7 (𝑓:𝐵𝐴 → ran 𝑓𝐴)
21adantr 481 . . . . . 6 ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → ran 𝑓𝐴)
3 ffn 6508 . . . . . . . . . . 11 (𝑓:𝐵𝐴𝑓 Fn 𝐵)
4 fnfvelrn 6841 . . . . . . . . . . 11 ((𝑓 Fn 𝐵𝑤𝐵) → (𝑓𝑤) ∈ ran 𝑓)
53, 4sylan 580 . . . . . . . . . 10 ((𝑓:𝐵𝐴𝑤𝐵) → (𝑓𝑤) ∈ ran 𝑓)
6 sseq2 3992 . . . . . . . . . . 11 (𝑠 = (𝑓𝑤) → (𝑧𝑠𝑧 ⊆ (𝑓𝑤)))
76rspcev 3622 . . . . . . . . . 10 (((𝑓𝑤) ∈ ran 𝑓𝑧 ⊆ (𝑓𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧𝑠)
85, 7sylan 580 . . . . . . . . 9 (((𝑓:𝐵𝐴𝑤𝐵) ∧ 𝑧 ⊆ (𝑓𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧𝑠)
98rexlimdva2 3287 . . . . . . . 8 (𝑓:𝐵𝐴 → (∃𝑤𝐵 𝑧 ⊆ (𝑓𝑤) → ∃𝑠 ∈ ran 𝑓 𝑧𝑠))
109ralimdv 3178 . . . . . . 7 (𝑓:𝐵𝐴 → (∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤) → ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))
1110imp 407 . . . . . 6 ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)
122, 11jca 512 . . . . 5 ((𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤)) → (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))
13 fvex 6677 . . . . . 6 (card‘ran 𝑓) ∈ V
14 cfval 9658 . . . . . . . . . . 11 (𝐴 ∈ On → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
1514adantr 481 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
16153ad2ant2 1126 . . . . . . . . 9 ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
17 vex 3498 . . . . . . . . . . . . . 14 𝑓 ∈ V
1817rnex 7605 . . . . . . . . . . . . 13 ran 𝑓 ∈ V
19 fveq2 6664 . . . . . . . . . . . . . . 15 (𝑦 = ran 𝑓 → (card‘𝑦) = (card‘ran 𝑓))
2019eqeq2d 2832 . . . . . . . . . . . . . 14 (𝑦 = ran 𝑓 → (𝑥 = (card‘𝑦) ↔ 𝑥 = (card‘ran 𝑓)))
21 sseq1 3991 . . . . . . . . . . . . . . 15 (𝑦 = ran 𝑓 → (𝑦𝐴 ↔ ran 𝑓𝐴))
22 rexeq 3407 . . . . . . . . . . . . . . . 16 (𝑦 = ran 𝑓 → (∃𝑠𝑦 𝑧𝑠 ↔ ∃𝑠 ∈ ran 𝑓 𝑧𝑠))
2322ralbidv 3197 . . . . . . . . . . . . . . 15 (𝑦 = ran 𝑓 → (∀𝑧𝐴𝑠𝑦 𝑧𝑠 ↔ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))
2421, 23anbi12d 630 . . . . . . . . . . . . . 14 (𝑦 = ran 𝑓 → ((𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠) ↔ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)))
2520, 24anbi12d 630 . . . . . . . . . . . . 13 (𝑦 = ran 𝑓 → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠)) ↔ (𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠))))
2618, 25spcev 3606 . . . . . . . . . . . 12 ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠)))
27 abid 2803 . . . . . . . . . . . 12 (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ↔ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠)))
2826, 27sylibr 235 . . . . . . . . . . 11 ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → 𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))})
29 intss1 4884 . . . . . . . . . . 11 (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ⊆ 𝑥)
3028, 29syl 17 . . . . . . . . . 10 ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ⊆ 𝑥)
31303adant2 1123 . . . . . . . . 9 ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑠𝑦 𝑧𝑠))} ⊆ 𝑥)
3216, 31eqsstrd 4004 . . . . . . . 8 ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ 𝑥)
33323expib 1114 . . . . . . 7 (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ 𝑥))
34 sseq2 3992 . . . . . . 7 (𝑥 = (card‘ran 𝑓) → ((cf‘𝐴) ⊆ 𝑥 ↔ (cf‘𝐴) ⊆ (card‘ran 𝑓)))
3533, 34sylibd 240 . . . . . 6 (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓)))
3613, 35vtocle 3584 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓𝐴 ∧ ∀𝑧𝐴𝑠 ∈ ran 𝑓 𝑧𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓))
3712, 36sylan2 592 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤))) → (cf‘𝐴) ⊆ (card‘ran 𝑓))
38 cardidm 9377 . . . . . . 7 (card‘(card‘ran 𝑓)) = (card‘ran 𝑓)
39 onss 7493 . . . . . . . . . . . . . 14 (𝐴 ∈ On → 𝐴 ⊆ On)
401, 39sylan9ssr 3980 . . . . . . . . . . . . 13 ((𝐴 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓 ⊆ On)
41403adant2 1123 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓 ⊆ On)
42 onssnum 9455 . . . . . . . . . . . 12 ((ran 𝑓 ∈ V ∧ ran 𝑓 ⊆ On) → ran 𝑓 ∈ dom card)
4318, 41, 42sylancr 587 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → ran 𝑓 ∈ dom card)
44 cardid2 9371 . . . . . . . . . . 11 (ran 𝑓 ∈ dom card → (card‘ran 𝑓) ≈ ran 𝑓)
4543, 44syl 17 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ≈ ran 𝑓)
46 onenon 9367 . . . . . . . . . . . . 13 (𝐵 ∈ On → 𝐵 ∈ dom card)
47 dffn4 6590 . . . . . . . . . . . . . 14 (𝑓 Fn 𝐵𝑓:𝐵onto→ran 𝑓)
483, 47sylib 219 . . . . . . . . . . . . 13 (𝑓:𝐵𝐴𝑓:𝐵onto→ran 𝑓)
49 fodomnum 9472 . . . . . . . . . . . . 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 8556 . . . . . . . . . 10 (((card‘ran 𝑓) ≈ ran 𝑓 ∧ ran 𝑓𝐵) → (card‘ran 𝑓) ≼ 𝐵)
5445, 52, 53syl2anc 584 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ≼ 𝐵)
55 cardon 9362 . . . . . . . . . . . 12 (card‘ran 𝑓) ∈ On
56 onenon 9367 . . . . . . . . . . . 12 ((card‘ran 𝑓) ∈ On → (card‘ran 𝑓) ∈ dom card)
5755, 56ax-mp 5 . . . . . . . . . . 11 (card‘ran 𝑓) ∈ dom card
58 carddom2 9395 . . . . . . . . . . 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 9375 . . . . . . . . 9 (𝐵 ∈ On → (card‘𝐵) ⊆ 𝐵)
63623ad2ant2 1126 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘𝐵) ⊆ 𝐵)
6461, 63sstrd 3976 . . . . . . 7 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘(card‘ran 𝑓)) ⊆ 𝐵)
6538, 64eqsstrrid 4015 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ⊆ 𝐵)
66653expa 1110 . . . . 5 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵𝐴) → (card‘ran 𝑓) ⊆ 𝐵)
6766adantrr 713 . . . 4 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵𝐴 ∧ ∀𝑧𝐴𝑤𝐵 𝑧 ⊆ (𝑓𝑤))) → (card‘ran 𝑓) ⊆ 𝐵)
6837, 67sstrd 3976 . . 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 2799  wral 3138  wrex 3139  Vcvv 3495  wss 3935   cint 4869   class class class wbr 5058  dom cdm 5549  ran crn 5550  Oncon0 6185   Fn wfn 6344  wf 6345  ontowfo 6347  cfv 6349  cen 8495  cdom 8496  cardccrd 9353  cfccf 9355
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 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  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 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-er 8279  df-map 8398  df-en 8499  df-dom 8500  df-sdom 8501  df-card 9357  df-cf 9359  df-acn 9360
This theorem is referenced by:  cfsmolem  9681  cfcoflem  9683  cfcof  9685  inar1  10186
  Copyright terms: Public domain W3C validator