Metamath Proof Explorer

Theorem eqsup

Description: Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis supmo.1 ⊢φ→ROrA
Assertion eqsup ⊢φ→C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→supBAR=C

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢φ→ROrA
2 1 adantr ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→ROrA
3 2 supval2 ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→supBAR=ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
4 3simpc ⊢C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz
5 4 adantl ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz
6 simpr1 ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→C∈A
7 breq1 ⊢x=C→xRy↔CRy
8 7 notbid ⊢x=C→¬xRy↔¬CRy
9 8 ralbidv ⊢x=C→∀y∈B¬xRy↔∀y∈B¬CRy
10 breq2 ⊢x=C→yRx↔yRC
11 10 imbi1d ⊢x=C→yRx→∃z∈ByRz↔yRC→∃z∈ByRz
12 11 ralbidv ⊢x=C→∀y∈AyRx→∃z∈ByRz↔∀y∈AyRC→∃z∈ByRz
13 9 12 anbi12d ⊢x=C→∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz↔∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz
14 13 rspcev ⊢C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
15 6 5 14 syl2anc ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
16 2 15 supeu ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
17 13 riota2 ⊢C∈A∧∃!x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz→∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz↔ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=C
18 6 16 17 syl2anc ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz↔ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=C
19 5 18 mpbid ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→ιx∈A|∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz=C
20 3 19 eqtrd ⊢φ∧C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→supBAR=C
21 20 ex ⊢φ→C∈A∧∀y∈B¬CRy∧∀y∈AyRC→∃z∈ByRz→supBAR=C