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	⊢ ( 𝜑 → ( 𝑆 𝑅 𝐶 ∨ 𝐶 = 𝑆 ) )