Metamath Proof Explorer

Theorem infglbb

Description: Bidirectional form of infglb . (Contributed by AV, 3-Sep-2020)

Ref Expression
Hypotheses infcl.1 ⊢φ→ROrA
infcl.2 ⊢φ→∃x∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy
infglbb.3 ⊢φ→B⊆A
Assertion infglbb ⊢φ∧C∈A→supBARRC↔∃z∈BzRC

Proof

Step Hyp Ref Expression
1 infcl.1 ⊢φ→ROrA
2 infcl.2 ⊢φ→∃x∈A∀y∈B¬yRx∧∀y∈AxRy→∃z∈BzRy
3 infglbb.3 ⊢φ→B⊆A
4 df-inf ⊢supBAR=supBAR-1
5 4 breq1i ⊢supBARRC↔supBAR-1RC
6 simpr ⊢φ∧C∈A→C∈A
7 cnvso ⊢ROrA↔R-1OrA
8 1 7 sylib ⊢φ→R-1OrA
9 1 2 infcllem ⊢φ→∃x∈A∀y∈B¬xR-1y∧∀y∈AyR-1x→∃z∈ByR-1z
10 8 9 supcl ⊢φ→supBAR-1∈A
11 10 adantr ⊢φ∧C∈A→supBAR-1∈A
12 brcnvg ⊢C∈A∧supBAR-1∈A→CR-1supBAR-1↔supBAR-1RC
13 12 bicomd ⊢C∈A∧supBAR-1∈A→supBAR-1RC↔CR-1supBAR-1
14 6 11 13 syl2anc ⊢φ∧C∈A→supBAR-1RC↔CR-1supBAR-1
15 8 9 3 suplub2 ⊢φ∧C∈A→CR-1supBAR-1↔∃z∈BCR-1z
16 vex ⊢z∈V
17 brcnvg ⊢C∈A∧z∈V→CR-1z↔zRC
18 6 16 17 sylancl ⊢φ∧C∈A→CR-1z↔zRC
19 18 rexbidv ⊢φ∧C∈A→∃z∈BCR-1z↔∃z∈BzRC
20 14 15 19 3bitrd ⊢φ∧C∈A→supBAR-1RC↔∃z∈BzRC
21 5 20 bitrid ⊢φ∧C∈A→supBARRC↔∃z∈BzRC