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
|- ( ( z = x /\ w = y ) -> ( ps <-> ch ) )
wlogle.2
|- ( ( z = y /\ w = x ) -> ( ps <-> th ) )
wlogle.3
|- ( ph -> S C_ RR )
wlogle.4
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( ch <-> th ) )
wlogle.5
|- ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> ch )
Assertion wlogle
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ch )

Proof

Step Hyp Ref Expression
1 wlogle.1
 |-  ( ( z = x /\ w = y ) -> ( ps <-> ch ) )
2 wlogle.2
 |-  ( ( z = y /\ w = x ) -> ( ps <-> th ) )
3 wlogle.3
 |-  ( ph -> S C_ RR )
4 wlogle.4
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( ch <-> th ) )
5 wlogle.5
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> ch )
6 4 3adantr3
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> ( ch <-> th ) )
7 5 6 mpbid
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> th )
8 1 2 3 7 5 wloglei
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ch )