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

Theorem infglbb 8394
Description: Bidirectional form of infglb 8393. (Contributed by AV, 3-Sep-2020.)
Hypotheses
Ref Expression
infcl.1 (𝜑𝑅 Or 𝐴)
infcl.2 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐵 𝑧𝑅𝑦)))
infglbb.3 (𝜑𝐵𝐴)
Assertion
Ref Expression
infglbb ((𝜑𝐶𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧𝐵 𝑧𝑅𝐶))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝑧,𝐶   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐶(𝑥,𝑦)

Proof of Theorem infglbb
StepHypRef Expression
1 df-inf 8346 . . 3 inf(𝐵, 𝐴, 𝑅) = sup(𝐵, 𝐴, 𝑅)
21breq1i 4658 . 2 (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)
3 simpr 477 . . . 4 ((𝜑𝐶𝐴) → 𝐶𝐴)
4 infcl.1 . . . . . . 7 (𝜑𝑅 Or 𝐴)
5 cnvso 5672 . . . . . . 7 (𝑅 Or 𝐴𝑅 Or 𝐴)
64, 5sylib 208 . . . . . 6 (𝜑𝑅 Or 𝐴)
7 infcl.2 . . . . . . 7 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐵 𝑧𝑅𝑦)))
84, 7infcllem 8390 . . . . . 6 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
96, 8supcl 8361 . . . . 5 (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)
109adantr 481 . . . 4 ((𝜑𝐶𝐴) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)
11 brcnvg 5301 . . . . 5 ((𝐶𝐴 ∧ sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
1211bicomd 213 . . . 4 ((𝐶𝐴 ∧ sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) → (sup(𝐵, 𝐴, 𝑅)𝑅𝐶𝐶𝑅sup(𝐵, 𝐴, 𝑅)))
133, 10, 12syl2anc 693 . . 3 ((𝜑𝐶𝐴) → (sup(𝐵, 𝐴, 𝑅)𝑅𝐶𝐶𝑅sup(𝐵, 𝐴, 𝑅)))
14 infglbb.3 . . . 4 (𝜑𝐵𝐴)
156, 8, 14suplub2 8364 . . 3 ((𝜑𝐶𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧𝐵 𝐶𝑅𝑧))
16 vex 3201 . . . . 5 𝑧 ∈ V
17 brcnvg 5301 . . . . 5 ((𝐶𝐴𝑧 ∈ V) → (𝐶𝑅𝑧𝑧𝑅𝐶))
183, 16, 17sylancl 694 . . . 4 ((𝜑𝐶𝐴) → (𝐶𝑅𝑧𝑧𝑅𝐶))
1918rexbidv 3050 . . 3 ((𝜑𝐶𝐴) → (∃𝑧𝐵 𝐶𝑅𝑧 ↔ ∃𝑧𝐵 𝑧𝑅𝐶))
2013, 15, 193bitrd 294 . 2 ((𝜑𝐶𝐴) → (sup(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧𝐵 𝑧𝑅𝐶))
212, 20syl5bb 272 1 ((𝜑𝐶𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧𝐵 𝑧𝑅𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wcel 1989  wral 2911  wrex 2912  Vcvv 3198  wss 3572   class class class wbr 4651   Or wor 5032  ccnv 5111  supcsup 8343  infcinf 8344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-po 5033  df-so 5034  df-cnv 5120  df-iota 5849  df-riota 6608  df-sup 8345  df-inf 8346
This theorem is referenced by:  infregelb  11004  infxrgelb  12162  infxrge0glb  29515  infxrglb  39375  infrglb  39628
  Copyright terms: Public domain W3C validator