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 bitrid ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ↔ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) )
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 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝜒 )