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 ) |
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 ) |