Step |
Hyp |
Ref |
Expression |
1 |
|
tgbtwnconn.p |
|- P = ( Base ` G ) |
2 |
|
tgbtwnconn.i |
|- I = ( Itv ` G ) |
3 |
|
tgbtwnconn.g |
|- ( ph -> G e. TarskiG ) |
4 |
|
tgbtwnconn.a |
|- ( ph -> A e. P ) |
5 |
|
tgbtwnconn.b |
|- ( ph -> B e. P ) |
6 |
|
tgbtwnconn.c |
|- ( ph -> C e. P ) |
7 |
|
tgbtwnconn.d |
|- ( ph -> D e. P ) |
8 |
|
tgbtwnconn3.1 |
|- ( ph -> B e. ( A I D ) ) |
9 |
|
tgbtwnconn3.2 |
|- ( ph -> C e. ( A I D ) ) |
10 |
|
eqid |
|- ( dist ` G ) = ( dist ` G ) |
11 |
3
|
adantr |
|- ( ( ph /\ ( # ` P ) = 1 ) -> G e. TarskiG ) |
12 |
5
|
adantr |
|- ( ( ph /\ ( # ` P ) = 1 ) -> B e. P ) |
13 |
4
|
adantr |
|- ( ( ph /\ ( # ` P ) = 1 ) -> A e. P ) |
14 |
6
|
adantr |
|- ( ( ph /\ ( # ` P ) = 1 ) -> C e. P ) |
15 |
|
simpr |
|- ( ( ph /\ ( # ` P ) = 1 ) -> ( # ` P ) = 1 ) |
16 |
1 10 2 11 12 13 14 15
|
tgldim0itv |
|- ( ( ph /\ ( # ` P ) = 1 ) -> B e. ( A I C ) ) |
17 |
16
|
orcd |
|- ( ( ph /\ ( # ` P ) = 1 ) -> ( B e. ( A I C ) \/ C e. ( A I B ) ) ) |
18 |
3
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> G e. TarskiG ) |
19 |
|
simplr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> p e. P ) |
20 |
4
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. P ) |
21 |
5
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> B e. P ) |
22 |
6
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> C e. P ) |
23 |
|
simprr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A =/= p ) |
24 |
23
|
necomd |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> p =/= A ) |
25 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> D e. P ) |
26 |
8
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> B e. ( A I D ) ) |
27 |
|
simprl |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( D I p ) ) |
28 |
1 10 2 18 25 20 19 27
|
tgbtwncom |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( p I D ) ) |
29 |
1 10 2 18 21 20 19 25 26 28
|
tgbtwnintr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( B I p ) ) |
30 |
1 10 2 18 21 20 19 29
|
tgbtwncom |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( p I B ) ) |
31 |
9
|
ad3antrrr |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> C e. ( A I D ) ) |
32 |
1 10 2 18 20 22 25 31
|
tgbtwncom |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> C e. ( D I A ) ) |
33 |
1 10 2 18 25 22 20 19 32 27
|
tgbtwnexch3 |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( C I p ) ) |
34 |
1 10 2 18 22 20 19 33
|
tgbtwncom |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> A e. ( p I C ) ) |
35 |
1 2 18 19 20 21 22 24 30 34
|
tgbtwnconn2 |
|- ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ p e. P ) /\ ( A e. ( D I p ) /\ A =/= p ) ) -> ( B e. ( A I C ) \/ C e. ( A I B ) ) ) |
36 |
3
|
adantr |
|- ( ( ph /\ 2 <_ ( # ` P ) ) -> G e. TarskiG ) |
37 |
7
|
adantr |
|- ( ( ph /\ 2 <_ ( # ` P ) ) -> D e. P ) |
38 |
4
|
adantr |
|- ( ( ph /\ 2 <_ ( # ` P ) ) -> A e. P ) |
39 |
|
simpr |
|- ( ( ph /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) ) |
40 |
1 10 2 36 37 38 39
|
tgbtwndiff |
|- ( ( ph /\ 2 <_ ( # ` P ) ) -> E. p e. P ( A e. ( D I p ) /\ A =/= p ) ) |
41 |
35 40
|
r19.29a |
|- ( ( ph /\ 2 <_ ( # ` P ) ) -> ( B e. ( A I C ) \/ C e. ( A I B ) ) ) |
42 |
1 4
|
tgldimor |
|- ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) ) |
43 |
17 41 42
|
mpjaodan |
|- ( ph -> ( B e. ( A I C ) \/ C e. ( A I B ) ) ) |