Metamath Proof Explorer

Theorem eqinf

Description: Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypothesis infexd.1 ⊢φ→ROrA
Assertion eqinf ⊢φ→C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy→supBAR=C

Proof

Step Hyp Ref Expression
1 infexd.1 ⊢φ→ROrA
2 df-inf ⊢supBAR=supBAR-1
3 cnvso ⊢ROrA↔R-1OrA
4 1 3 sylib ⊢φ→R-1OrA
5 4 eqsup ⊢φ→C∈A∧∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z→supBAR-1=C
6 brcnvg ⊢C∈A∧y∈V→CR-1y↔yRC
7 6 bicomd ⊢C∈A∧y∈V→yRC↔CR-1y
8 7 elvd ⊢C∈A→yRC↔CR-1y
9 8 notbid ⊢C∈A→¬yRC↔¬CR-1y
10 9 ralbidv ⊢C∈A→∀y∈B¬yRC↔∀y∈B¬CR-1y
11 vex ⊢y∈V
12 brcnvg ⊢y∈V∧C∈A→yR-1C↔CRy
13 11 12 mpan ⊢C∈A→yR-1C↔CRy
14 13 bicomd ⊢C∈A→CRy↔yR-1C
15 vex ⊢z∈V
16 11 15 brcnv ⊢yR-1z↔zRy
17 16 a1i ⊢C∈A→yR-1z↔zRy
18 17 bicomd ⊢C∈A→zRy↔yR-1z
19 18 rexbidv ⊢C∈A→∃z∈BzRy↔∃z∈ByR-1z
20 14 19 imbi12d ⊢C∈A→CRy→∃z∈BzRy↔yR-1C→∃z∈ByR-1z
21 20 ralbidv ⊢C∈A→∀y∈ACRy→∃z∈BzRy↔∀y∈AyR-1C→∃z∈ByR-1z
22 10 21 anbi12d ⊢C∈A→∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy↔∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z
23 22 pm5.32i ⊢C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy↔C∈A∧∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z
24 3anass ⊢C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy↔C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy
25 3anass ⊢C∈A∧∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z↔C∈A∧∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z
26 23 24 25 3bitr4i ⊢C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy↔C∈A∧∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z
27 26 biimpi ⊢C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy→C∈A∧∀y∈B¬CR-1y∧∀y∈AyR-1C→∃z∈ByR-1z
28 5 27 impel ⊢φ∧C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy→supBAR-1=C
29 2 28 eqtrid ⊢φ∧C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy→supBAR=C
30 29 ex ⊢φ→C∈A∧∀y∈B¬yRC∧∀y∈ACRy→∃z∈BzRy→supBAR=C