Metamath Proof Explorer

Theorem supubt

Description: Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion supubt ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→C∈B→¬supBARRC

Proof

Step Hyp Ref Expression
1 simpl ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→ROrA
2 simpr ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
3 1 2 supub ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→C∈B→¬supBARRC