Metamath Proof Explorer

Theorem supub

Description: A supremum is an upper bound. See also supcl and suplub .

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

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

Ref Expression
Hypotheses supmo.1 ⊢φ→ROrA
supcl.2 ⊢φ→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
Assertion supub ⊢φ→C∈B→¬supBARRC

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢φ→ROrA
2 supcl.2 ⊢φ→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
3 simpl ⊢∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∀y∈B¬xRy
4 3 a1i ⊢x∈A→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∀y∈B¬xRy
5 4 ss2rabi ⊢x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz⊆x∈A|∀y∈B¬xRy
6 1 supval2 ⊢φ→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
7 1 2 supeu ⊢φ→∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
8 riotacl2 ⊢∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz∈x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
9 7 8 syl ⊢φ→ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz∈x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
10 6 9 eqeltrd ⊢φ→supBAR∈x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
11 5 10 sselid ⊢φ→supBAR∈x∈A|∀y∈B¬xRy
12 breq2 ⊢y=w→xRy↔xRw
13 12 notbid ⊢y=w→¬xRy↔¬xRw
14 13 cbvralvw ⊢∀y∈B¬xRy↔∀w∈B¬xRw
15 breq1 ⊢x=supBAR→xRw↔supBARRw
16 15 notbid ⊢x=supBAR→¬xRw↔¬supBARRw
17 16 ralbidv ⊢x=supBAR→∀w∈B¬xRw↔∀w∈B¬supBARRw
18 14 17 bitrid ⊢x=supBAR→∀y∈B¬xRy↔∀w∈B¬supBARRw
19 18 elrab ⊢supBAR∈x∈A|∀y∈B¬xRy↔supBAR∈A∧∀w∈B¬supBARRw
20 19 simprbi ⊢supBAR∈x∈A|∀y∈B¬xRy→∀w∈B¬supBARRw
21 11 20 syl ⊢φ→∀w∈B¬supBARRw
22 breq2 ⊢w=C→supBARRw↔supBARRC
23 22 notbid ⊢w=C→¬supBARRw↔¬supBARRC
24 23 rspccv ⊢∀w∈B¬supBARRw→C∈B→¬supBARRC
25 21 24 syl ⊢φ→C∈B→¬supBARRC