Metamath Proof Explorer

Theorem infglbb

Description: Bidirectional form of infglb . (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
infglbb.3 ⊢ φ → B ⊆ A
Assertion infglbb ⊢ φ ∧ 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 infglbb.3 ⊢ φ → B ⊆ A
4 df-inf ⊢ sup B A R = sup B A R -1
5 4 breq1i ⊢ sup B A R R C ↔ sup B A R -1 R C
6 simpr ⊢ φ ∧ C ∈ A → C ∈ A
7 cnvso ⊢ R Or A ↔ R -1 Or A
8 1 7 sylib ⊢ φ → R -1 Or A
9 1 2 infcllem ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
10 8 9 supcl ⊢ φ → sup B A R -1 ∈ A
11 10 adantr ⊢ φ ∧ C ∈ A → sup B A R -1 ∈ A
12 brcnvg ⊢ C ∈ A ∧ sup B A R -1 ∈ A → C R -1 sup B A R -1 ↔ sup B A R -1 R C
13 12 bicomd ⊢ C ∈ A ∧ sup B A R -1 ∈ A → sup B A R -1 R C ↔ C R -1 sup B A R -1
14 6 11 13 syl2anc ⊢ φ ∧ C ∈ A → sup B A R -1 R C ↔ C R -1 sup B A R -1
15 8 9 3 suplub2 ⊢ φ ∧ C ∈ A → C R -1 sup B A R -1 ↔ ∃ z ∈ B C R -1 z
16 vex ⊢ z ∈ V
17 brcnvg ⊢ C ∈ A ∧ z ∈ V → C R -1 z ↔ z R C
18 6 16 17 sylancl ⊢ φ ∧ C ∈ A → C R -1 z ↔ z R C
19 18 rexbidv ⊢ φ ∧ C ∈ A → ∃ z ∈ B C R -1 z ↔ ∃ z ∈ B z R C
20 14 15 19 3bitrd ⊢ φ ∧ C ∈ A → sup B A R -1 R C ↔ ∃ z ∈ B z R C
21 5 20 bitrid ⊢ φ ∧ C ∈ A → sup B A R R C ↔ ∃ z ∈ B z R C