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

Metamath Proof Explorer

Theorem infltoreq

Description: The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020)

Ref Expression
Hypotheses infltoreq.1 ⊢ φ → R Or A
infltoreq.2 ⊢ φ → B ⊆ A
infltoreq.3 ⊢ φ → B ∈ Fin
infltoreq.4 ⊢ φ → C ∈ B
infltoreq.5 ⊢ φ → S = inf B A R
Assertion infltoreq ⊢ φ → S R C ∨ C = S

Proof

Step Hyp Ref Expression
1 infltoreq.1 ⊢ φ → R Or A
2 infltoreq.2 ⊢ φ → B ⊆ A
3 infltoreq.3 ⊢ φ → B ∈ Fin
4 infltoreq.4 ⊢ φ → C ∈ B
5 infltoreq.5 ⊢ φ → S = inf B A R
6 cnvso ⊢ R Or A ↔ R -1 Or A
7 1 6 sylib ⊢ φ → R -1 Or A
8 df-inf ⊢ inf B A R = sup B A R -1
9 5 8 eqtrdi ⊢ φ → S = sup B A R -1
10 7 2 3 4 9 supgtoreq ⊢ φ → C R -1 S ∨ C = S
11 4 ne0d ⊢ φ → B ≠ ∅
12 fiinfcl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → inf B A R ∈ B
13 1 3 11 2 12 syl13anc ⊢ φ → inf B A R ∈ B
14 5 13 eqeltrd ⊢ φ → S ∈ B
15 brcnvg ⊢ C ∈ B ∧ S ∈ B → C R -1 S ↔ S R C
16 15 bicomd ⊢ C ∈ B ∧ S ∈ B → S R C ↔ C R -1 S
17 4 14 16 syl2anc ⊢ φ → S R C ↔ C R -1 S
18 17 orbi1d ⊢ φ → S R C ∨ C = S ↔ C R -1 S ∨ C = S
19 10 18 mpbird ⊢ φ → S R C ∨ C = S