Metamath Proof Explorer

Theorem suplub2

Description: Bidirectional form of suplub . (Contributed by Mario Carneiro, 6-Sep-2014)

Ref Expression
Hypotheses supmo.1 ⊢φ→ROrA
supcl.2 ⊢φ→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
suplub2.3 ⊢φ→B⊆A
Assertion suplub2 ⊢φ∧C∈A→CRsupBAR↔∃z∈BCRz

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢φ→ROrA
2 supcl.2 ⊢φ→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
3 suplub2.3 ⊢φ→B⊆A
4 1 2 suplub ⊢φ→C∈A∧CRsupBAR→∃z∈BCRz
5 4 expdimp ⊢φ∧C∈A→CRsupBAR→∃z∈BCRz
6 breq2 ⊢z=w→CRz↔CRw
7 6 cbvrexvw ⊢∃z∈BCRz↔∃w∈BCRw
8 breq2 ⊢supBAR=w→CRsupBAR↔CRw
9 8 biimprd ⊢supBAR=w→CRw→CRsupBAR
10 9 a1i ⊢φ∧C∈A∧w∈B→supBAR=w→CRw→CRsupBAR
11 1 ad2antrr ⊢φ∧C∈A∧w∈B→ROrA
12 simplr ⊢φ∧C∈A∧w∈B→C∈A
13 3 adantr ⊢φ∧C∈A→B⊆A
14 13 sselda ⊢φ∧C∈A∧w∈B→w∈A
15 1 2 supcl ⊢φ→supBAR∈A
16 15 ad2antrr ⊢φ∧C∈A∧w∈B→supBAR∈A
17 sotr ⊢ROrA∧C∈A∧w∈A∧supBAR∈A→CRw∧wRsupBAR→CRsupBAR
18 11 12 14 16 17 syl13anc ⊢φ∧C∈A∧w∈B→CRw∧wRsupBAR→CRsupBAR
19 18 expcomd ⊢φ∧C∈A∧w∈B→wRsupBAR→CRw→CRsupBAR
20 1 2 supub ⊢φ→w∈B→¬supBARRw
21 20 adantr ⊢φ∧C∈A→w∈B→¬supBARRw
22 21 imp ⊢φ∧C∈A∧w∈B→¬supBARRw
23 sotric ⊢ROrA∧supBAR∈A∧w∈A→supBARRw↔¬supBAR=w∨wRsupBAR
24 11 16 14 23 syl12anc ⊢φ∧C∈A∧w∈B→supBARRw↔¬supBAR=w∨wRsupBAR
25 24 con2bid ⊢φ∧C∈A∧w∈B→supBAR=w∨wRsupBAR↔¬supBARRw
26 22 25 mpbird ⊢φ∧C∈A∧w∈B→supBAR=w∨wRsupBAR
27 10 19 26 mpjaod ⊢φ∧C∈A∧w∈B→CRw→CRsupBAR
28 27 rexlimdva ⊢φ∧C∈A→∃w∈BCRw→CRsupBAR
29 7 28 biimtrid ⊢φ∧C∈A→∃z∈BCRz→CRsupBAR
30 5 29 impbid ⊢φ∧C∈A→CRsupBAR↔∃z∈BCRz