Description: The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008) (Proof shortened by OpenAI, 30-Mar-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | supmax.1 | ⊢ ( 𝜑 → 𝑅 Or 𝐴 ) | |
| supmax.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) | ||
| supmax.3 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | ||
| supmax.4 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝐶 𝑅 𝑦 ) | ||
| Assertion | supmax | ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | supmax.1 | ⊢ ( 𝜑 → 𝑅 Or 𝐴 ) | |
| 2 | supmax.2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 ) | |
| 3 | supmax.3 | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | |
| 4 | supmax.4 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝐶 𝑅 𝑦 ) | |
| 5 | simprr | ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝐶 ) ) → 𝑦 𝑅 𝐶 ) | |
| 6 | breq2 | ⊢ ( 𝑧 = 𝐶 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝐶 ) ) | |
| 7 | 6 | rspcev | ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝑦 𝑅 𝐶 ) → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) |
| 8 | 3 5 7 | syl2an2r | ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝐶 ) ) → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) |
| 9 | 1 2 4 8 | eqsupd | ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) |