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 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
infltoreq.2 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
infltoreq.3 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
infltoreq.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
infltoreq.5 ⊢ ( 𝜑 → 𝑆 = inf ( 𝐵 , 𝐴 , 𝑅 ) )
Assertion infltoreq ( 𝜑 → ( 𝑆 𝑅 𝐶 ∨ 𝐶 = 𝑆 ) )

Proof

Step Hyp Ref Expression
1 infltoreq.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 infltoreq.2 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3 infltoreq.3 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
4 infltoreq.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
5 infltoreq.5 ⊢ ( 𝜑 → 𝑆 = inf ( 𝐵 , 𝐴 , 𝑅 ) )
6 cnvso ⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
7 1 6 sylib ⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
8 df-inf ⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
9 5 8 eqtrdi ⊢ ( 𝜑 → 𝑆 = sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) )
10 7 2 3 4 9 supgtoreq ⊢ ( 𝜑 → ( 𝐶 ◡ 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )
11 4 ne0d ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
12 fiinfcl ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
13 1 3 11 2 12 syl13anc ⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
14 5 13 eqeltrd ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
15 brcnvg ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝑆 ∈ 𝐵 ) → ( 𝐶 ◡ 𝑅 𝑆 ↔ 𝑆 𝑅 𝐶 ) )
16 15 bicomd ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝑆 ∈ 𝐵 ) → ( 𝑆 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 𝑆 ) )
17 4 14 16 syl2anc ⊢ ( 𝜑 → ( 𝑆 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 𝑆 ) )
18 17 orbi1d ⊢ ( 𝜑 → ( ( 𝑆 𝑅 𝐶 ∨ 𝐶 = 𝑆 ) ↔ ( 𝐶 ◡ 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) ) )
19 10 18 mpbird ⊢ ( 𝜑 → ( 𝑆 𝑅 𝐶 ∨ 𝐶 = 𝑆 ) )