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

Theorem glbval 17351
 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 253 . . . . 5 ((∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))
5 glbva.k . . . . . 6 (𝜑𝐾𝑉)
65adantr 474 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → 𝐾𝑉)
71, 2, 3, 4, 6glbfval 17345 . . . 4 ((𝜑𝑆 ∈ dom 𝐺) → 𝐺 = ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))}))
87fveq1d 6436 . . 3 ((𝜑𝑆 ∈ dom 𝐺) → (𝐺𝑆) = (((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})‘𝑆))
9 glbval.p . . . . . 6 (𝜓 ↔ (∀𝑦𝑆 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
10 simpr 479 . . . . . 6 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆 ∈ dom 𝐺)
111, 2, 3, 9, 6, 10glbeu 17350 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → ∃!𝑥𝐵 𝜓)
12 raleq 3351 . . . . . . . . . 10 (𝑠 = 𝑆 → (∀𝑦𝑠 𝑥 𝑦 ↔ ∀𝑦𝑆 𝑥 𝑦))
13 raleq 3351 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (∀𝑦𝑠 𝑧 𝑦 ↔ ∀𝑦𝑆 𝑧 𝑦))
1413imbi1d 333 . . . . . . . . . . 11 (𝑠 = 𝑆 → ((∀𝑦𝑠 𝑧 𝑦𝑧 𝑥) ↔ (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
1514ralbidv 3196 . . . . . . . . . 10 (𝑠 = 𝑆 → (∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥) ↔ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥)))
1612, 15anbi12d 626 . . . . . . . . 9 (𝑠 = 𝑆 → ((∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ (∀𝑦𝑆 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑧 𝑦𝑧 𝑥))))
1716, 9syl6bbr 281 . . . . . . . 8 (𝑠 = 𝑆 → ((∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ 𝜓))
1817reubidv 3339 . . . . . . 7 (𝑠 = 𝑆 → (∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)) ↔ ∃!𝑥𝐵 𝜓))
1918elabg 3570 . . . . . 6 (𝑆 ∈ dom 𝐺 → (𝑆 ∈ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))} ↔ ∃!𝑥𝐵 𝜓))
2019adantl 475 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → (𝑆 ∈ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))} ↔ ∃!𝑥𝐵 𝜓))
2111, 20mpbird 249 . . . 4 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆 ∈ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})
22 fvres 6453 . . . 4 (𝑆 ∈ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))} → (((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆))
2321, 22syl 17 . . 3 ((𝜑𝑆 ∈ dom 𝐺) → (((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) ↾ {𝑠 ∣ ∃!𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))})‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆))
24 glbval.ss . . . . . 6 (𝜑𝑆𝐵)
2524adantr 474 . . . . 5 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆𝐵)
261fvexi 6448 . . . . . 6 𝐵 ∈ V
2726elpw2 5051 . . . . 5 (𝑆 ∈ 𝒫 𝐵𝑆𝐵)
2825, 27sylibr 226 . . . 4 ((𝜑𝑆 ∈ dom 𝐺) → 𝑆 ∈ 𝒫 𝐵)
2917riotabidv 6869 . . . . 5 (𝑠 = 𝑆 → (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))) = (𝑥𝐵 𝜓))
30 eqid 2826 . . . . 5 (𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥)))) = (𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))
31 riotaex 6871 . . . . 5 (𝑥𝐵 𝜓) ∈ V
3229, 30, 31fvmpt 6530 . . . 4 (𝑆 ∈ 𝒫 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆) = (𝑥𝐵 𝜓))
3328, 32syl 17 . . 3 ((𝜑𝑆 ∈ dom 𝐺) → ((𝑠 ∈ 𝒫 𝐵 ↦ (𝑥𝐵 (∀𝑦𝑠 𝑥 𝑦 ∧ ∀𝑧𝐵 (∀𝑦𝑠 𝑧 𝑦𝑧 𝑥))))‘𝑆) = (𝑥𝐵 𝜓))
348, 23, 333eqtrd 2866 . 2 ((𝜑𝑆 ∈ dom 𝐺) → (𝐺𝑆) = (𝑥𝐵 𝜓))
35 ndmfv 6464 . . . 4 𝑆 ∈ dom 𝐺 → (𝐺𝑆) = ∅)
3635adantl 475 . . 3 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → (𝐺𝑆) = ∅)
371, 2, 3, 9, 5glbeldm 17348 . . . . . . 7 (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆𝐵 ∧ ∃!𝑥𝐵 𝜓)))
3837biimprd 240 . . . . . 6 (𝜑 → ((𝑆𝐵 ∧ ∃!𝑥𝐵 𝜓) → 𝑆 ∈ dom 𝐺))
3924, 38mpand 688 . . . . 5 (𝜑 → (∃!𝑥𝐵 𝜓𝑆 ∈ dom 𝐺))
4039con3dimp 399 . . . 4 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → ¬ ∃!𝑥𝐵 𝜓)
41 riotaund 6903 . . . 4 (¬ ∃!𝑥𝐵 𝜓 → (𝑥𝐵 𝜓) = ∅)
4240, 41syl 17 . . 3 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → (𝑥𝐵 𝜓) = ∅)
4336, 42eqtr4d 2865 . 2 ((𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺) → (𝐺𝑆) = (𝑥𝐵 𝜓))
4434, 43pm2.61dan 849 1 (𝜑 → (𝐺𝑆) = (𝑥𝐵 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1658   ∈ wcel 2166  {cab 2812  ∀wral 3118  ∃!wreu 3120   ⊆ wss 3799  ∅c0 4145  𝒫 cpw 4379   class class class wbr 4874   ↦ cmpt 4953  dom cdm 5343   ↾ cres 5345  ‘cfv 6124  ℩crio 6866  Basecbs 16223  lecple 16313  glbcglb 17297 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-reu 3125  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-riota 6867  df-glb 17329 This theorem is referenced by:  glbcl  17352  glbprop  17353  meetval2  17377  isglbd  17471  tosglb  30216  glb0N  35269  glbconN  35453
 Copyright terms: Public domain W3C validator