Metamath Proof Explorer

Theorem inflb

Description: An infimum is a lower bound. See also infcl and infglb . (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 inflb ⊢ φ → C ∈ B → ¬ C R inf B A R

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 cnvso ⊢ R Or A ↔ R -1 Or A
4 1 3 sylib ⊢ φ → R -1 Or A
5 1 2 infcllem ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R -1 y ∧ ∀ y ∈ A y R -1 x → ∃ z ∈ B y R -1 z
6 4 5 supub ⊢ φ → C ∈ B → ¬ sup B A R -1 R -1 C
7 6 imp ⊢ φ ∧ C ∈ B → ¬ sup B A R -1 R -1 C
8 df-inf ⊢ inf B A R = sup B A R -1
9 8 a1i ⊢ φ ∧ C ∈ B → inf B A R = sup B A R -1
10 9 breq2d ⊢ φ ∧ C ∈ B → C R inf B A R ↔ C R sup B A R -1
11 4 5 supcl ⊢ φ → sup B A R -1 ∈ A
12 brcnvg ⊢ sup B A R -1 ∈ A ∧ C ∈ B → sup B A R -1 R -1 C ↔ C R sup B A R -1
13 12 bicomd ⊢ sup B A R -1 ∈ A ∧ C ∈ B → C R sup B A R -1 ↔ sup B A R -1 R -1 C
14 11 13 sylan ⊢ φ ∧ C ∈ B → C R sup B A R -1 ↔ sup B A R -1 R -1 C
15 10 14 bitrd ⊢ φ ∧ C ∈ B → C R inf B A R ↔ sup B A R -1 R -1 C
16 7 15 mtbird ⊢ φ ∧ C ∈ B → ¬ C R inf B A R
17 16 ex ⊢ φ → C ∈ B → ¬ C R inf B A R