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

Theorem supub 8316
Description: A supremum is an upper bound. See also supcl 8315 and suplub 8317.

This proof demonstrates how to expand an iota-based definition (df-iota 5815) using riotacl2 6584.

(Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)

Hypotheses
Ref Expression
supmo.1 (𝜑𝑅 Or 𝐴)
supcl.2 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
Assertion
Ref Expression
supub (𝜑 → (𝐶𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝑅,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝐶(𝑥,𝑦,𝑧)

Proof of Theorem supub
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 simpl 473 . . . . . 6 ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)
21a1i 11 . . . . 5 (𝑥𝐴 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → ∀𝑦𝐵 ¬ 𝑥𝑅𝑦))
32ss2rabi 3668 . . . 4 {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))} ⊆ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦}
4 supmo.1 . . . . . 6 (𝜑𝑅 Or 𝐴)
54supval2 8312 . . . . 5 (𝜑 → sup(𝐵, 𝐴, 𝑅) = (𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
6 supcl.2 . . . . . . 7 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
74, 6supeu 8311 . . . . . 6 (𝜑 → ∃!𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
8 riotacl2 6584 . . . . . 6 (∃!𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ∈ {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))})
97, 8syl 17 . . . . 5 (𝜑 → (𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ∈ {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))})
105, 9eqeltrd 2698 . . . 4 (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))})
113, 10sseldi 3585 . . 3 (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦})
12 breq2 4622 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥𝑅𝑦𝑥𝑅𝑤))
1312notbid 308 . . . . . . 7 (𝑦 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑤))
1413cbvralv 3162 . . . . . 6 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤𝐵 ¬ 𝑥𝑅𝑤)
15 breq1 4621 . . . . . . . 8 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (𝑥𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1615notbid 308 . . . . . . 7 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (¬ 𝑥𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1716ralbidv 2981 . . . . . 6 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑤𝐵 ¬ 𝑥𝑅𝑤 ↔ ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1814, 17syl5bb 272 . . . . 5 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1918elrab 3350 . . . 4 (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦} ↔ (sup(𝐵, 𝐴, 𝑅) ∈ 𝐴 ∧ ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
2019simprbi 480 . . 3 (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦} → ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
2111, 20syl 17 . 2 (𝜑 → ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
22 breq2 4622 . . . 4 (𝑤 = 𝐶 → (sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
2322notbid 308 . . 3 (𝑤 = 𝐶 → (¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
2423rspccv 3295 . 2 (∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 → (𝐶𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
2521, 24syl 17 1 (𝜑 → (𝐶𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  ∃!wreu 2909  {crab 2911   class class class wbr 4618   Or wor 4999  crio 6570  supcsup 8297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-po 5000  df-so 5001  df-iota 5815  df-riota 6571  df-sup 8299
This theorem is referenced by:  suplub2  8318  supgtoreq  8327  supiso  8332  inflb  8346  suprub  10935  suprzub  11730  supxrun  12096  supxrub  12104  dgrub  23907  supssd  29348  ssnnssfz  29409  oddpwdc  30215  itg2addnclem  33120  supubt  33193  ssnn0ssfz  41436
  Copyright terms: Public domain W3C validator