Metamath Proof Explorer

Theorem infval

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

Ref Expression
Hypothesis infexd.1 ⊢ φ → R Or A
Assertion infval ⊢ φ → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y

Proof

Step Hyp Ref Expression
1 infexd.1 ⊢ φ → R Or A
2 df-inf ⊢ sup B A R = sup B A R -1
3 cnvso ⊢ R Or A ↔ R -1 Or A
4 1 3 sylib ⊢ φ → R -1 Or A
5 4 supval2 ⊢ φ → sup B A R -1 = ι x ∈ A | ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
6 vex ⊢ x ∈ V
7 vex ⊢ y ∈ V
8 6 7 brcnv ⊢ x R -1 y ↔ y R x
9 8 a1i ⊢ φ → x R -1 y ↔ y R x
10 9 notbid ⊢ φ → ¬ x R -1 y ↔ ¬ y R x
11 10 ralbidv ⊢ φ → ∀ y ∈ B ¬ x R -1 y ↔ ∀ y ∈ B ¬ y R x
12 7 6 brcnv ⊢ y R -1 x ↔ x R y
13 12 a1i ⊢ φ → y R -1 x ↔ x R y
14 vex ⊢ z ∈ V
15 7 14 brcnv ⊢ y R -1 z ↔ z R y
16 15 a1i ⊢ φ → y R -1 z ↔ z R y
17 16 rexbidv ⊢ φ → ∃ z ∈ B y R -1 z ↔ ∃ z ∈ B z R y
18 13 17 imbi12d ⊢ φ → y R -1 x → ∃ z ∈ B y R -1 z ↔ x R y → ∃ z ∈ B z R y
19 18 ralbidv ⊢ φ → ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z ↔ ∀ y ∈ A x R y → ∃ z ∈ B z R y
20 11 19 anbi12d ⊢ φ → ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z ↔ ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
21 20 riotabidv ⊢ φ → ι x ∈ A | ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z = ι x ∈ A | ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
22 5 21 eqtrd ⊢ φ → sup B A R -1 = ι x ∈ A | ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
23 2 22 eqtrid ⊢ φ → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y