Description: If the predicate ch ( x , y ) is symmetric under interchange of x , y , then "without loss of generality" we can assume that x <_ y . (Contributed by Mario Carneiro, 18-Aug-2014) (Revised by Mario Carneiro, 11-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wlogle.1 | ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| wlogle.2 | ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( 𝜓 ↔ 𝜃 ) ) | ||
| wlogle.3 | ⊢ ( 𝜑 → 𝑆 ⊆ ℝ ) | ||
| wlogle.4 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝜒 ↔ 𝜃 ) ) | ||
| wlogle.5 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦 ) ) → 𝜒 ) | ||
| Assertion | wlogle | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝜒 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlogle.1 | ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 2 | wlogle.2 | ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( 𝜓 ↔ 𝜃 ) ) | |
| 3 | wlogle.3 | ⊢ ( 𝜑 → 𝑆 ⊆ ℝ ) | |
| 4 | wlogle.4 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝜒 ↔ 𝜃 ) ) | |
| 5 | wlogle.5 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦 ) ) → 𝜒 ) | |
| 6 | 4 | 3adantr3 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦 ) ) → ( 𝜒 ↔ 𝜃 ) ) |
| 7 | 5 6 | mpbid | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑥 ≤ 𝑦 ) ) → 𝜃 ) |
| 8 | 1 2 3 7 5 | wloglei | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝜒 ) |