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