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 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝜒 ) |