Metamath Proof Explorer


Theorem wlogle

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

Proof

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