Metamath Proof Explorer

Theorem infval

Description: Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypothesis infexd.1 ⊢φ→ROrA
Assertion infval ⊢φ→supBAR=ιx∈A|∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy

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 supval2 ⊢φ→supBAR-1=ιx∈A|∀y∈B¬xR-1y∧∀y∈AyR-1x→∃z∈ByR-1z
6 vex ⊢x∈V
7 vex ⊢y∈V
8 6 7 brcnv ⊢xR-1y↔yRx
9 8 a1i ⊢φ→xR-1y↔yRx
10 9 notbid ⊢φ→¬xR-1y↔¬yRx
11 10 ralbidv ⊢φ→∀y∈B¬xR-1y↔∀y∈B¬yRx
12 7 6 brcnv ⊢yR-1x↔xRy
13 12 a1i ⊢φ→yR-1x↔xRy
14 vex ⊢z∈V
15 7 14 brcnv ⊢yR-1z↔zRy
16 15 a1i ⊢φ→yR-1z↔zRy
17 16 rexbidv ⊢φ→∃z∈ByR-1z↔∃z∈BzRy
18 13 17 imbi12d ⊢φ→yR-1x→∃z∈ByR-1z↔xRy→∃z∈BzRy
19 18 ralbidv ⊢φ→∀y∈AyR-1x→∃z∈ByR-1z↔∀y∈AxRy→∃z∈BzRy
20 11 19 anbi12d ⊢φ→∀y∈B¬xR-1y∧∀y∈AyR-1x→∃z∈ByR-1z↔∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy
21 20 riotabidv ⊢φ→ιx∈A|∀y∈B¬xR-1y∧∀y∈AyR-1x→∃z∈ByR-1z=ιx∈A|∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy
22 5 21 eqtrd ⊢φ→supBAR-1=ιx∈A|∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy
23 2 22 eqtrid ⊢φ→supBAR=ιx∈A|∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy