Theorem fiinfcl

Description: A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Assertion	fiinfcl	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
2		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
3		fisupcl	⊢ ( ( ◡ 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐵 )
4	2 3	sylanb	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐵 )
5	1 4	eqeltrid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )