Description: Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishlg.p | |
|
ishlg.i | |
||
ishlg.k | |
||
ishlg.a | |
||
ishlg.b | |
||
ishlg.c | |
||
hlln.1 | |
||
hltr.d | |
||
btwnhl.1 | |
||
btwnhl.3 | |
||
Assertion | btwnhl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishlg.p | |
|
2 | ishlg.i | |
|
3 | ishlg.k | |
|
4 | ishlg.a | |
|
5 | ishlg.b | |
|
6 | ishlg.c | |
|
7 | hlln.1 | |
|
8 | hltr.d | |
|
9 | btwnhl.1 | |
|
10 | btwnhl.3 | |
|
11 | eqid | |
|
12 | 7 | adantr | |
13 | 6 | adantr | |
14 | 8 | adantr | |
15 | 5 | adantr | |
16 | 4 | adantr | |
17 | 1 2 3 4 5 8 7 | ishlg | |
18 | 9 17 | mpbid | |
19 | 18 | simp1d | |
20 | 19 | necomd | |
21 | 20 | adantr | |
22 | 10 | adantr | |
23 | 1 11 2 12 16 14 13 22 | tgbtwncom | |
24 | simpr | |
|
25 | 1 11 2 12 13 14 16 15 21 23 24 | tgbtwnouttr | |
26 | 1 11 2 12 13 14 15 25 | tgbtwncom | |
27 | 7 | adantr | |
28 | 4 | adantr | |
29 | 5 | adantr | |
30 | 8 | adantr | |
31 | 6 | adantr | |
32 | simpr | |
|
33 | 1 11 2 27 30 29 28 32 | tgbtwncom | |
34 | 10 | adantr | |
35 | 1 11 2 27 28 29 30 31 33 34 | tgbtwnexch3 | |
36 | 18 | simp3d | |
37 | 26 35 36 | mpjaodan | |