Metamath Proof Explorer

Theorem wloglei

Description: Form of wlogle where both sides of the equivalence are proven rather than showing that they are equivalent to each other. (Contributed by Mario Carneiro, 9-Mar-2015)

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 )
wloglei.4 
|- ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> th )
wloglei.5 
|- ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> ch )
Assertion wloglei 
|- ( ( 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 wloglei.4 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> th )
5 wloglei.5 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ x <_ y ) ) -> ch )
6 3 adantr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> S C_ RR )
7 simprr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> y e. S )
8 6 7 sseldd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> y e. RR )
9 simprl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> x e. S )
10 6 9 sseldd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> x e. RR )
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 eleq1w 
 |-  ( z = x -> ( z e. S <-> x e. S ) )
14 eleq1w 
 |-  ( w = y -> ( w e. S <-> y e. S ) )
15 13 14 bi2anan9 
 |-  ( ( z = x /\ w = y ) -> ( ( z e. S /\ w e. S ) <-> ( x e. S /\ y e. S ) ) )
16 15 anbi2d 
 |-  ( ( z = x /\ w = y ) -> ( ( ph /\ ( z e. S /\ w e. S ) ) <-> ( ph /\ ( x e. S /\ y e. S ) ) ) )
17 breq12 
 |-  ( ( w = y /\ z = x ) -> ( w <_ z <-> y <_ x ) )
18 17 ancoms 
 |-  ( ( z = x /\ w = y ) -> ( w <_ z <-> y <_ x ) )
19 16 18 anbi12d 
 |-  ( ( z = x /\ w = y ) -> ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ w <_ z ) <-> ( ( ph /\ ( x e. S /\ y e. S ) ) /\ y <_ x ) ) )
20 19 1 imbi12d 
 |-  ( ( z = x /\ w = y ) -> ( ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ w <_ z ) -> ps ) <-> ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ y <_ x ) -> ch ) ) )
21 vex 
 |-  z e. _V
22 vex 
 |-  w e. _V
23 ancom 
 |-  ( ( x e. S /\ y e. S ) <-> ( y e. S /\ x e. S ) )
24 eleq1w 
 |-  ( y = z -> ( y e. S <-> z e. S ) )
25 eleq1w 
 |-  ( x = w -> ( x e. S <-> w e. S ) )
26 24 25 bi2anan9 
 |-  ( ( y = z /\ x = w ) -> ( ( y e. S /\ x e. S ) <-> ( z e. S /\ w e. S ) ) )
27 23 26 bitrid 
 |-  ( ( y = z /\ x = w ) -> ( ( x e. S /\ y e. S ) <-> ( z e. S /\ w e. S ) ) )
28 27 anbi2d 
 |-  ( ( y = z /\ x = w ) -> ( ( ph /\ ( x e. S /\ y e. S ) ) <-> ( ph /\ ( z e. S /\ w e. S ) ) ) )
29 breq12 
 |-  ( ( x = w /\ y = z ) -> ( x <_ y <-> w <_ z ) )
30 29 ancoms 
 |-  ( ( y = z /\ x = w ) -> ( x <_ y <-> w <_ z ) )
31 28 30 anbi12d 
 |-  ( ( y = z /\ x = w ) -> ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ x <_ y ) <-> ( ( ph /\ ( z e. S /\ w e. S ) ) /\ w <_ z ) ) )
32 equcom 
 |-  ( y = z <-> z = y )
33 equcom 
 |-  ( x = w <-> w = x )
34 32 33 2 syl2anb 
 |-  ( ( y = z /\ x = w ) -> ( ps <-> th ) )
35 34 bicomd 
 |-  ( ( y = z /\ x = w ) -> ( th <-> ps ) )
36 31 35 imbi12d 
 |-  ( ( y = z /\ x = w ) -> ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ x <_ y ) -> th ) <-> ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ w <_ z ) -> ps ) ) )
37 df-3an 
 |-  ( ( x e. S /\ y e. S /\ x <_ y ) <-> ( ( x e. S /\ y e. S ) /\ x <_ y ) )
38 37 4 sylan2br 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ x <_ y ) ) -> th )
39 38 anassrs 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ x <_ y ) -> th )
40 21 22 36 39 vtocl2 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ w <_ z ) -> ps )
41 11 12 20 40 vtocl2 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ y <_ x ) -> ch )
42 37 5 sylan2br 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ x <_ y ) ) -> ch )
43 42 anassrs 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ x <_ y ) -> ch )
44 8 10 41 43 lecasei 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ch )