Description: A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | fiinfcl | ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 ) |
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 ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 ) |