Description: The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by AV, 3-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | infmin.1 | ⊢ ( 𝜑 → 𝑅 Or 𝐴 ) | |
| infmin.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) | ||
| infmin.3 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | ||
| infmin.4 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑦 𝑅 𝐶 ) | ||
| Assertion | infmin | ⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | infmin.1 | ⊢ ( 𝜑 → 𝑅 Or 𝐴 ) | |
| 2 | infmin.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) | |
| 3 | infmin.3 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | |
| 4 | infmin.4 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑦 𝑅 𝐶 ) | |
| 5 | simprr | ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝐶 𝑅 𝑦 ) ) → 𝐶 𝑅 𝑦 ) | |
| 6 | breq1 | ⊢ ( 𝑧 = 𝐶 → ( 𝑧 𝑅 𝑦 ↔ 𝐶 𝑅 𝑦 ) ) | |
| 7 | 6 | rspcev | ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐶 𝑅 𝑦 ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) |
| 8 | 3 5 7 | syl2an2r | ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝐶 𝑅 𝑦 ) ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) |
| 9 | 1 2 4 8 | eqinfd | ⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) |