Metamath Proof Explorer

Theorem infglb

Description: An infimum is the greatest lower bound. See also infcl and inflb . (Contributed by AV, 3-Sep-2020)

Ref Expression
Hypotheses infcl.1 ⊢ φ → R Or A
infcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
Assertion infglb ⊢ φ → C ∈ A ∧ sup B A R R C → ∃ z ∈ B z R C

Proof

Step Hyp Ref Expression
1 infcl.1 ⊢ φ → R Or A
2 infcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
3 df-inf ⊢ sup B A R = sup B A R -1
4 3 breq1i ⊢ sup B A R R C ↔ sup B A R -1 R C
5 simpr ⊢ φ ∧ C ∈ A → C ∈ A
6 cnvso ⊢ R Or A ↔ R -1 Or A
7 1 6 sylib ⊢ φ → R -1 Or A
8 1 2 infcllem ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
9 7 8 supcl ⊢ φ → sup B A R -1 ∈ A
10 9 adantr ⊢ φ ∧ C ∈ A → sup B A R -1 ∈ A
11 brcnvg ⊢ C ∈ A ∧ sup B A R -1 ∈ A → C R -1 sup B A R -1 ↔ sup B A R -1 R C
12 11 bicomd ⊢ C ∈ A ∧ sup B A R -1 ∈ A → sup B A R -1 R C ↔ C R -1 sup B A R -1
13 5 10 12 syl2anc ⊢ φ ∧ C ∈ A → sup B A R -1 R C ↔ C R -1 sup B A R -1
14 4 13 bitrid ⊢ φ ∧ C ∈ A → sup B A R R C ↔ C R -1 sup B A R -1
15 7 8 suplub ⊢ φ → C ∈ A ∧ C R -1 sup B A R -1 → ∃ z ∈ B C R -1 z
16 15 expdimp ⊢ φ ∧ C ∈ A → C R -1 sup B A R -1 → ∃ z ∈ B C R -1 z
17 vex ⊢ z ∈ V
18 brcnvg ⊢ C ∈ A ∧ z ∈ V → C R -1 z ↔ z R C
19 5 17 18 sylancl ⊢ φ ∧ C ∈ A → C R -1 z ↔ z R C
20 19 rexbidv ⊢ φ ∧ C ∈ A → ∃ z ∈ B C R -1 z ↔ ∃ z ∈ B z R C
21 16 20 sylibd ⊢ φ ∧ C ∈ A → C R -1 sup B A R -1 → ∃ z ∈ B z R C
22 14 21 sylbid ⊢ φ ∧ C ∈ A → sup B A R R C → ∃ z ∈ B z R C
23 22 expimpd ⊢ φ → C ∈ A ∧ sup B A R R C → ∃ z ∈ B z R C