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 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( 𝜓𝜒 ) )
wlogle.2 ( ( 𝑧 = 𝑦𝑤 = 𝑥 ) → ( 𝜓𝜃 ) )
wlogle.3 ( 𝜑𝑆 ⊆ ℝ )
wloglei.4 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑥𝑦 ) ) → 𝜃 )
wloglei.5 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑥𝑦 ) ) → 𝜒 )
Assertion wloglei ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 wlogle.1 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( 𝜓𝜒 ) )
2 wlogle.2 ( ( 𝑧 = 𝑦𝑤 = 𝑥 ) → ( 𝜓𝜃 ) )
3 wlogle.3 ( 𝜑𝑆 ⊆ ℝ )
4 wloglei.4 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑥𝑦 ) ) → 𝜃 )
5 wloglei.5 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑥𝑦 ) ) → 𝜒 )
6 3 adantr ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑆 ⊆ ℝ )
7 simprr ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑦𝑆 )
8 6 7 sseldd ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑦 ∈ ℝ )
9 simprl ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑥𝑆 )
10 6 9 sseldd ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝑥 ∈ ℝ )
11 vex 𝑥 ∈ V
12 vex 𝑦 ∈ V
13 eleq1w ( 𝑧 = 𝑥 → ( 𝑧𝑆𝑥𝑆 ) )
14 eleq1w ( 𝑤 = 𝑦 → ( 𝑤𝑆𝑦𝑆 ) )
15 13 14 bi2anan9 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ( 𝑧𝑆𝑤𝑆 ) ↔ ( 𝑥𝑆𝑦𝑆 ) ) )
16 15 anbi2d ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ↔ ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ) )
17 breq12 ( ( 𝑤 = 𝑦𝑧 = 𝑥 ) → ( 𝑤𝑧𝑦𝑥 ) )
18 17 ancoms ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( 𝑤𝑧𝑦𝑥 ) )
19 16 18 anbi12d ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ( ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ∧ 𝑤𝑧 ) ↔ ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑦𝑥 ) ) )
20 19 1 imbi12d ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ( ( ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ∧ 𝑤𝑧 ) → 𝜓 ) ↔ ( ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑦𝑥 ) → 𝜒 ) ) )
21 vex 𝑧 ∈ V
22 vex 𝑤 ∈ V
23 ancom ( ( 𝑥𝑆𝑦𝑆 ) ↔ ( 𝑦𝑆𝑥𝑆 ) )
24 eleq1w ( 𝑦 = 𝑧 → ( 𝑦𝑆𝑧𝑆 ) )
25 eleq1w ( 𝑥 = 𝑤 → ( 𝑥𝑆𝑤𝑆 ) )
26 24 25 bi2anan9 ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( ( 𝑦𝑆𝑥𝑆 ) ↔ ( 𝑧𝑆𝑤𝑆 ) ) )
27 23 26 syl5bb ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( ( 𝑥𝑆𝑦𝑆 ) ↔ ( 𝑧𝑆𝑤𝑆 ) ) )
28 27 anbi2d ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ↔ ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ) )
29 breq12 ( ( 𝑥 = 𝑤𝑦 = 𝑧 ) → ( 𝑥𝑦𝑤𝑧 ) )
30 29 ancoms ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( 𝑥𝑦𝑤𝑧 ) )
31 28 30 anbi12d ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑥𝑦 ) ↔ ( ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ∧ 𝑤𝑧 ) ) )
32 equcom ( 𝑦 = 𝑧𝑧 = 𝑦 )
33 equcom ( 𝑥 = 𝑤𝑤 = 𝑥 )
34 32 33 2 syl2anb ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( 𝜓𝜃 ) )
35 34 bicomd ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( 𝜃𝜓 ) )
36 31 35 imbi12d ( ( 𝑦 = 𝑧𝑥 = 𝑤 ) → ( ( ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑥𝑦 ) → 𝜃 ) ↔ ( ( ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ∧ 𝑤𝑧 ) → 𝜓 ) ) )
37 df-3an ( ( 𝑥𝑆𝑦𝑆𝑥𝑦 ) ↔ ( ( 𝑥𝑆𝑦𝑆 ) ∧ 𝑥𝑦 ) )
38 37 4 sylan2br ( ( 𝜑 ∧ ( ( 𝑥𝑆𝑦𝑆 ) ∧ 𝑥𝑦 ) ) → 𝜃 )
39 38 anassrs ( ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑥𝑦 ) → 𝜃 )
40 21 22 36 39 vtocl2 ( ( ( 𝜑 ∧ ( 𝑧𝑆𝑤𝑆 ) ) ∧ 𝑤𝑧 ) → 𝜓 )
41 11 12 20 40 vtocl2 ( ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑦𝑥 ) → 𝜒 )
42 37 5 sylan2br ( ( 𝜑 ∧ ( ( 𝑥𝑆𝑦𝑆 ) ∧ 𝑥𝑦 ) ) → 𝜒 )
43 42 anassrs ( ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) ∧ 𝑥𝑦 ) → 𝜒 )
44 8 10 41 43 lecasei ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝜒 )