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 ⊢ φ → R Or A
infcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
Assertion infnlb ⊢ φ → C ∈ A ∧ ∀ z ∈ B ¬ z R C → ¬ inf B A R 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 1 2 infglb ⊢ φ → C ∈ A ∧ inf B A R R C → ∃ z ∈ B z R C
4 3 expdimp ⊢ φ ∧ C ∈ A → inf B A R R C → ∃ z ∈ B z R C
5 dfrex2 ⊢ ∃ z ∈ B z R C ↔ ¬ ∀ z ∈ B ¬ z R C
6 4 5 imbitrdi ⊢ φ ∧ C ∈ A → inf B A R R C → ¬ ∀ z ∈ B ¬ z R C
7 6 con2d ⊢ φ ∧ C ∈ A → ∀ z ∈ B ¬ z R C → ¬ inf B A R R C
8 7 expimpd ⊢ φ → C ∈ A ∧ ∀ z ∈ B ¬ z R C → ¬ inf B A R R C