Metamath Proof Explorer

Theorem supval2

Description: Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016) (Revised by Thierry Arnoux, 24-Sep-2017)

Ref Expression
Hypothesis supmo.1 ⊢φ→ROrA
Assertion supval2 ⊢φ→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢φ→ROrA
2 df-sup ⊢supBAR=⋃x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
3 simpl ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→ROrA
4 simpr ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
5 3 4 supeu ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
6 riotauni ⊢∃!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
7 5 6 syl ⊢ROrA∧∃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
8 2 7 eqtr4id ⊢ROrA∧∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
9 rabn0 ⊢x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz≠∅↔∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
10 9 necon1bbii ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz↔x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=∅
11 10 biimpi ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=∅
12 11 unieqd ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→⋃x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=⋃∅
13 uni0 ⊢⋃∅=∅
14 12 13 eqtrdi ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→⋃x∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=∅
15 2 14 eqtrid ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→supBAR=∅
16 reurex ⊢∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
17 riotaund ⊢¬∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=∅
18 16 17 nsyl5 ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=∅
19 15 18 eqtr4d ⊢¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
20 19 adantl ⊢ROrA∧¬∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
21 8 20 pm2.61dan ⊢ROrA→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
22 1 21 syl ⊢φ→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz