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

Theorem supssd 30764
Description: Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.)
Hypotheses
Ref Expression
supssd.0 (𝜑𝑅 Or 𝐴)
supssd.1 (𝜑𝐵𝐶)
supssd.2 (𝜑𝐶𝐴)
supssd.3 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
supssd.4 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧)))
Assertion
Ref Expression
supssd (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem supssd
StepHypRef Expression
1 supssd.0 . . 3 (𝜑𝑅 Or 𝐴)
2 supssd.4 . . 3 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧)))
31, 2supcl 9074 . 2 (𝜑 → sup(𝐶, 𝐴, 𝑅) ∈ 𝐴)
4 supssd.1 . . . . 5 (𝜑𝐵𝐶)
54sseld 3900 . . . 4 (𝜑 → (𝑧𝐵𝑧𝐶))
61, 2supub 9075 . . . 4 (𝜑 → (𝑧𝐶 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑧))
75, 6syld 47 . . 3 (𝜑 → (𝑧𝐵 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑧))
87ralrimiv 3104 . 2 (𝜑 → ∀𝑧𝐵 ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑧)
9 supssd.3 . . 3 (𝜑 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
101, 9supnub 9078 . 2 (𝜑 → ((sup(𝐶, 𝐴, 𝑅) ∈ 𝐴 ∧ ∀𝑧𝐵 ¬ sup(𝐶, 𝐴, 𝑅)𝑅𝑧) → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅)))
113, 8, 10mp2and 699 1 (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wcel 2110  wral 3061  wrex 3062  wss 3866   class class class wbr 5053   Or wor 5467  supcsup 9056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-po 5468  df-so 5469  df-iota 6338  df-riota 7170  df-sup 9058
This theorem is referenced by:  xrsupssd  30802
  Copyright terms: Public domain W3C validator