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 ( 𝜑𝑅 Or 𝐴 )
infcl.2 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐵 𝑧 𝑅 𝑦 ) ) )
Assertion infglb ( 𝜑 → ( ( 𝐶𝐴 ∧ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) → ∃ 𝑧𝐵 𝑧 𝑅 𝐶 ) )

Proof

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