Metamath Proof Explorer


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 ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )