Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tosglb Structured version   Visualization version   GIF version

Theorem tosglb 30791
 Description: Same theorem as toslub 30789, for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018.) (Revised by AV, 28-Sep-2020.)
Hypotheses
Ref Expression
tosglb.b 𝐵 = (Base‘𝐾)
tosglb.l < = (lt‘𝐾)
tosglb.1 (𝜑𝐾 ∈ Toset)
tosglb.2 (𝜑𝐴𝐵)
Assertion
Ref Expression
tosglb (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < ))

Proof of Theorem tosglb
Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tosglb.b . . . . 5 𝐵 = (Base‘𝐾)
2 tosglb.l . . . . 5 < = (lt‘𝐾)
3 tosglb.1 . . . . 5 (𝜑𝐾 ∈ Toset)
4 tosglb.2 . . . . 5 (𝜑𝐴𝐵)
5 eqid 2758 . . . . 5 (le‘𝐾) = (le‘𝐾)
61, 2, 3, 4, 5tosglblem 30790 . . . 4 ((𝜑𝑎𝐵) → ((∀𝑏𝐴 𝑎(le‘𝐾)𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐(le‘𝐾)𝑏𝑐(le‘𝐾)𝑎)) ↔ (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
76riotabidva 7133 . . 3 (𝜑 → (𝑎𝐵 (∀𝑏𝐴 𝑎(le‘𝐾)𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐(le‘𝐾)𝑏𝑐(le‘𝐾)𝑎))) = (𝑎𝐵 (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
8 eqid 2758 . . . 4 (glb‘𝐾) = (glb‘𝐾)
9 biid 264 . . . 4 ((∀𝑏𝐴 𝑎(le‘𝐾)𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐(le‘𝐾)𝑏𝑐(le‘𝐾)𝑎)) ↔ (∀𝑏𝐴 𝑎(le‘𝐾)𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐(le‘𝐾)𝑏𝑐(le‘𝐾)𝑎)))
101, 5, 8, 9, 3, 4glbval 17686 . . 3 (𝜑 → ((glb‘𝐾)‘𝐴) = (𝑎𝐵 (∀𝑏𝐴 𝑎(le‘𝐾)𝑏 ∧ ∀𝑐𝐵 (∀𝑏𝐴 𝑐(le‘𝐾)𝑏𝑐(le‘𝐾)𝑎))))
111, 5, 2tosso 17725 . . . . . . 7 (𝐾 ∈ Toset → (𝐾 ∈ Toset ↔ ( < Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ (le‘𝐾))))
1211ibi 270 . . . . . 6 (𝐾 ∈ Toset → ( < Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ (le‘𝐾)))
1312simpld 498 . . . . 5 (𝐾 ∈ Toset → < Or 𝐵)
14 cnvso 6122 . . . . 5 ( < Or 𝐵 < Or 𝐵)
1513, 14sylib 221 . . . 4 (𝐾 ∈ Toset → < Or 𝐵)
16 id 22 . . . . 5 ( < Or 𝐵 < Or 𝐵)
1716supval2 8965 . . . 4 ( < Or 𝐵 → sup(𝐴, 𝐵, < ) = (𝑎𝐵 (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
183, 15, 173syl 18 . . 3 (𝜑 → sup(𝐴, 𝐵, < ) = (𝑎𝐵 (∀𝑏𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏𝐵 (𝑏 < 𝑎 → ∃𝑑𝐴 𝑏 < 𝑑))))
197, 10, 183eqtr4d 2803 . 2 (𝜑 → ((glb‘𝐾)‘𝐴) = sup(𝐴, 𝐵, < ))
20 df-inf 8953 . . . 4 inf(𝐴, 𝐵, < ) = sup(𝐴, 𝐵, < )
2120eqcomi 2767 . . 3 sup(𝐴, 𝐵, < ) = inf(𝐴, 𝐵, < )
2221a1i 11 . 2 (𝜑 → sup(𝐴, 𝐵, < ) = inf(𝐴, 𝐵, < ))
2319, 22eqtrd 2793 1 (𝜑 → ((glb‘𝐾)‘𝐴) = inf(𝐴, 𝐵, < ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071   ⊆ wss 3860   class class class wbr 5036   I cid 5433   Or wor 5446  ◡ccnv 5527   ↾ cres 5530  ‘cfv 6340  ℩crio 7113  supcsup 8950  infcinf 8951  Basecbs 16554  lecple 16643  ltcplt 17630  glbcglb 17632  Tosetctos 17722 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-sup 8952  df-inf 8953  df-proset 17617  df-poset 17635  df-plt 17647  df-glb 17664  df-toset 17723 This theorem is referenced by:  xrsp0  30828
 Copyright terms: Public domain W3C validator