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

Theorem supub 8635
Description: A supremum is an upper bound. See also supcl 8634 and suplub 8636.

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

(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 476 . . . . . 6 ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)
21a1i 11 . . . . 5 (𝑥𝐴 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → ∀𝑦𝐵 ¬ 𝑥𝑅𝑦))
32ss2rabi 3910 . . . 4 {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))} ⊆ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦}
4 supmo.1 . . . . . 6 (𝜑𝑅 Or 𝐴)
54supval2 8631 . . . . 5 (𝜑 → sup(𝐵, 𝐴, 𝑅) = (𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
6 supcl.2 . . . . . . 7 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
74, 6supeu 8630 . . . . . 6 (𝜑 → ∃!𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
8 riotacl2 6880 . . . . . 6 (∃!𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) → (𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ∈ {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))})
97, 8syl 17 . . . . 5 (𝜑 → (𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))) ∈ {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))})
105, 9eqeltrd 2907 . . . 4 (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))})
113, 10sseldi 3826 . . 3 (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦})
12 breq2 4878 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥𝑅𝑦𝑥𝑅𝑤))
1312notbid 310 . . . . . . 7 (𝑦 = 𝑤 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑅𝑤))
1413cbvralv 3384 . . . . . 6 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤𝐵 ¬ 𝑥𝑅𝑤)
15 breq1 4877 . . . . . . . 8 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (𝑥𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1615notbid 310 . . . . . . 7 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (¬ 𝑥𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1716ralbidv 3196 . . . . . 6 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑤𝐵 ¬ 𝑥𝑅𝑤 ↔ ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1814, 17syl5bb 275 . . . . 5 (𝑥 = sup(𝐵, 𝐴, 𝑅) → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
1918elrab 3586 . . . 4 (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦} ↔ (sup(𝐵, 𝐴, 𝑅) ∈ 𝐴 ∧ ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤))
2019simprbi 492 . . 3 (sup(𝐵, 𝐴, 𝑅) ∈ {𝑥𝐴 ∣ ∀𝑦𝐵 ¬ 𝑥𝑅𝑦} → ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
2111, 20syl 17 . 2 (𝜑 → ∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤)
22 breq2 4878 . . . 4 (𝑤 = 𝐶 → (sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
2322notbid 310 . . 3 (𝑤 = 𝐶 → (¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 ↔ ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
2423rspccv 3524 . 2 (∀𝑤𝐵 ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝑤 → (𝐶𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
2521, 24syl 17 1 (𝜑 → (𝐶𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386   = wceq 1658  wcel 2166  wral 3118  wrex 3119  ∃!wreu 3120  {crab 3122   class class class wbr 4874   Or wor 5263  crio 6866  supcsup 8616
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-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  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-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-po 5264  df-so 5265  df-iota 6087  df-riota 6867  df-sup 8618
This theorem is referenced by:  suplub2  8637  supgtoreq  8646  supiso  8651  inflb  8665  suprub  11315  suprzub  12063  supxrun  12435  supxrub  12443  dgrub  24390  supssd  30036  ssnnssfz  30097  oddpwdc  30962  itg2addnclem  34005  supubt  34078  ssnn0ssfz  42975
  Copyright terms: Public domain W3C validator