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