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

Theorem glbval 17603
Description: Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying 𝑆 ∈ dom 𝑈) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
Hypotheses
Ref Expression
glbval.b 𝐵 = (Base‘𝐾)
glbval.l = (le‘𝐾)
glbval.g 𝐺 = (glb‘𝐾)
glbval.p (𝜓 ↔ (∀𝑦𝑆 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
glbva.k (𝜑𝐾𝑉)
glbval.ss (𝜑𝑆𝐵)
Assertion
Ref Expression
glbval (𝜑 → (𝐺𝑆) = (𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝑧,𝐵   𝑥,𝑦,𝐾,𝑧   𝑥,𝑆,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)   𝐵(𝑦)   𝐺(𝑥,𝑦,𝑧)   (𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem glbval
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 glbval.b . . . . 5 𝐵 = (Base‘𝐾)
2 glbval.l . . . . 5 = (le‘𝐾)
3 glbval.g . . . . 5 𝐺 = (glb‘𝐾)
4 biid 264 . . . . 5 ((∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))
5 glbva.k . . . . . 6 (𝜑𝐾𝑉)
65adantr 484 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → 𝐾𝑉)
71, 2, 3, 4, 6glbfval 17597 . . . 4 ((𝜑𝑆 ∈ dom 𝐺) → 𝐺 = ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))}))
87fveq1d 6660 . . 3 ((𝜑𝑆 ∈ dom 𝐺) → (𝐺𝑆) = (((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})‘𝑆))
9 simpr 488 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆 ∈ dom 𝐺)
10 glbval.p . . . . . 6 (𝜓 ↔ (∀𝑦𝑆 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
111, 2, 3, 10, 6, 9glbeu 17602 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → ∃!𝑥𝐵 𝜓)
12 raleq 3397 . . . . . . . 8 (𝑠 = 𝑆 → (∀𝑦𝑠 𝑥 𝑦 ↔ ∀𝑦𝑆 𝑥 𝑦))
13 raleq 3397 . . . . . . . . . 10 (𝑠 = 𝑆 → (∀𝑦𝑠 𝑧 𝑦 ↔ ∀𝑦𝑆 𝑧 𝑦))
1413imbi1d 345 . . . . . . . . 9 (𝑠 = 𝑆 → ((∀𝑦𝑠 𝑧 𝑦𝑧 𝑥) ↔ (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
1514ralbidv 3192 . . . . . . . 8 (𝑠 = 𝑆 → (∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥) ↔ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
1612, 15anbi12d 633 . . . . . . 7 (𝑠 = 𝑆 → ((∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ (∀𝑦𝑆 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥))))
1716, 10syl6bbr 292 . . . . . 6 (𝑠 = 𝑆 → ((∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ 𝜓))
1817reubidv 3381 . . . . 5 (𝑠 = 𝑆 → (∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ ∃!𝑥𝐵 𝜓))
199, 11, 18elabd 3655 . . . 4 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆 ∈ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})
2019fvresd 6678 . . 3 ((𝜑𝑆 ∈ dom 𝐺) → (((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆))
21 glbval.ss . . . . . 6 (𝜑𝑆𝐵)
2221adantr 484 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆𝐵)
231fvexi 6672 . . . . . 6 𝐵 ∈ V
2423elpw2 5234 . . . . 5 (𝑆 ∈ 𝒫 𝐵𝑆𝐵)
2522, 24sylibr 237 . . . 4 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆 ∈ 𝒫 𝐵)
2617riotabidv 7105 . . . . 5 (𝑠 = 𝑆 → (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))) = (𝑥𝐵 𝜓))
27 eqid 2824 . . . . 5 (𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) = (𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))
28 riotaex 7107 . . . . 5 (𝑥𝐵 𝜓) ∈ V
2926, 27, 28fvmpt 6756 . . . 4 (𝑆 ∈ 𝒫 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆) = (𝑥𝐵 𝜓))
3025, 29syl 17 . . 3 ((𝜑𝑆 ∈ dom 𝐺) → ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆) = (𝑥𝐵 𝜓))
318, 20, 303eqtrd 2863 . 2 ((𝜑𝑆 ∈ dom 𝐺) → (𝐺𝑆) = (𝑥𝐵 𝜓))
32 ndmfv 6688 . . . 4 𝑆 ∈ dom 𝐺 → (𝐺𝑆) = ∅)
3332adantl 485 . . 3 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → (𝐺𝑆) = ∅)
341, 2, 3, 10, 5glbeldm 17600 . . . . . . 7 (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆𝐵 ∧ ∃!𝑥𝐵 𝜓)))
3534biimprd 251 . . . . . 6 (𝜑 → ((𝑆𝐵 ∧ ∃!𝑥𝐵 𝜓) → 𝑆 ∈ dom 𝐺))
3621, 35mpand 694 . . . . 5 (𝜑 → (∃!𝑥𝐵 𝜓𝑆 ∈ dom 𝐺))
3736con3dimp 412 . . . 4 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → ¬ ∃!𝑥𝐵 𝜓)
38 riotaund 7142 . . . 4 (¬ ∃!𝑥𝐵 𝜓 → (𝑥𝐵 𝜓) = ∅)
3937, 38syl 17 . . 3 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → (𝑥𝐵 𝜓) = ∅)
4033, 39eqtr4d 2862 . 2 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → (𝐺𝑆) = (𝑥𝐵 𝜓))
4131, 40pm2.61dan 812 1 (𝜑 → (𝐺𝑆) = (𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  {cab 2802  wral 3133  ∃!wreu 3135  wss 3919  c0 4275  𝒫 cpw 4521   class class class wbr 5052  cmpt 5132  dom cdm 5542  cres 5544  cfv 6343  crio 7102  Basecbs 16479  lecple 16568  glbcglb 17549
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 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  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 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7103  df-glb 17581
This theorem is referenced by:  glbcl  17604  glbprop  17605  meetval2  17629  isglbd  17723  tosglb  30661  glb0N  36399  glbconN  36583
  Copyright terms: Public domain W3C validator