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 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝜒 ) |