Metamath Proof Explorer


Theorem infglbb

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

Ref Expression
Hypotheses infcl.1 ( 𝜑𝑅 Or 𝐴 )
infcl.2 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐵 𝑧 𝑅 𝑦 ) ) )
infglbb.3 ( 𝜑𝐵𝐴 )
Assertion infglbb ( ( 𝜑𝐶𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧𝐵 𝑧 𝑅 𝐶 ) )

Proof

Step Hyp Ref Expression
1 infcl.1 ( 𝜑𝑅 Or 𝐴 )
2 infcl.2 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐵 𝑧 𝑅 𝑦 ) ) )
3 infglbb.3 ( 𝜑𝐵𝐴 )
4 df-inf inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , 𝑅 )
5 4 breq1i ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 )
6 simpr ( ( 𝜑𝐶𝐴 ) → 𝐶𝐴 )
7 cnvso ( 𝑅 Or 𝐴 𝑅 Or 𝐴 )
8 1 7 sylib ( 𝜑 𝑅 Or 𝐴 )
9 1 2 infcllem ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
10 8 9 supcl ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )
11 10 adantr ( ( 𝜑𝐶𝐴 ) → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )
12 brcnvg ( ( 𝐶𝐴 ∧ sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )
13 12 bicomd ( ( 𝐶𝐴 ∧ sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
14 6 11 13 syl2anc ( ( 𝜑𝐶𝐴 ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
15 8 9 3 suplub2 ( ( 𝜑𝐶𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∃ 𝑧𝐵 𝐶 𝑅 𝑧 ) )
16 vex 𝑧 ∈ V
17 brcnvg ( ( 𝐶𝐴𝑧 ∈ V ) → ( 𝐶 𝑅 𝑧𝑧 𝑅 𝐶 ) )
18 6 16 17 sylancl ( ( 𝜑𝐶𝐴 ) → ( 𝐶 𝑅 𝑧𝑧 𝑅 𝐶 ) )
19 18 rexbidv ( ( 𝜑𝐶𝐴 ) → ( ∃ 𝑧𝐵 𝐶 𝑅 𝑧 ↔ ∃ 𝑧𝐵 𝑧 𝑅 𝐶 ) )
20 14 15 19 3bitrd ( ( 𝜑𝐶𝐴 ) → ( sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧𝐵 𝑧 𝑅 𝐶 ) )
21 5 20 syl5bb ( ( 𝜑𝐶𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ ∃ 𝑧𝐵 𝑧 𝑅 𝐶 ) )