This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infnlb

Description: A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 infcl.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 infcl.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
3 1 2 infglb ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
4 3 expdimp ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
5 dfrex2 ⊢ ( ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ↔ ¬ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 )
6 4 5 imbitrdi ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 → ¬ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 ) )
7 6 con2d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 → ¬ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )
8 7 expimpd ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 ) → ¬ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )