Proof of Theorem tgbtwnconn1lem1
Step | Hyp | Ref
| Expression |
1 | | tgbtwnconn1.p |
. 2
|
2 | | tgbtwnconn1.m |
. 2
|
3 | | tgbtwnconn1.i |
. 2
Itv |
4 | | tgbtwnconn1.g |
. 2
TarskiG |
5 | | tgbtwnconn1.b |
. 2
|
6 | | tgbtwnconn1.j |
. 2
|
7 | | tgbtwnconn1.a |
. 2
|
8 | | tgbtwnconn1.h |
. 2
|
9 | | tgbtwnconn1.1 |
. 2
|
10 | | tgbtwnconn1.e |
. . 3
|
11 | | tgbtwnconn1.d |
. . . 4
|
12 | | tgbtwnconn1.3 |
. . . 4
|
13 | | tgbtwnconn1.4 |
. . . 4
|
14 | 1, 2, 3, 4, 7, 5, 11, 10, 12, 13 | tgbtwnexch 25393 |
. . 3
|
15 | | tgbtwnconn1.6 |
. . 3
|
16 | 1, 2, 3, 4, 7, 5, 10, 8, 14, 15 | tgbtwnexch 25393 |
. 2
|
17 | | tgbtwnconn1.f |
. . 3
|
18 | | tgbtwnconn1.c |
. . . 4
|
19 | | tgbtwnconn1.2 |
. . . 4
|
20 | | tgbtwnconn1.5 |
. . . 4
|
21 | 1, 2, 3, 4, 7, 5, 18, 17, 19, 20 | tgbtwnexch 25393 |
. . 3
|
22 | | tgbtwnconn1.7 |
. . 3
|
23 | 1, 2, 3, 4, 7, 5, 17, 6, 21, 22 | tgbtwnexch 25393 |
. 2
|
24 | 1, 2, 3, 4, 7, 5, 10, 8, 14, 15 | tgbtwnexch3 25389 |
. . 3
|
25 | 1, 2, 3, 4, 7, 18,
17, 6, 20, 22 | tgbtwnexch 25393 |
. . . . 5
|
26 | 1, 2, 3, 4, 7, 5, 18, 6, 19, 25 | tgbtwnexch3 25389 |
. . . 4
|
27 | 1, 2, 3, 4, 5, 18,
6, 26 | tgbtwncom 25383 |
. . 3
|
28 | 1, 2, 3, 4, 7, 5, 11, 10, 12, 13 | tgbtwnexch3 25389 |
. . . 4
|
29 | 1, 2, 3, 4, 7, 18,
17, 6, 20, 22 | tgbtwnexch3 25389 |
. . . . 5
|
30 | 1, 2, 3, 4, 18, 17, 6, 29 | tgbtwncom 25383 |
. . . 4
|
31 | 1, 2, 3, 4, 6, 17 | axtgcgrrflx 25361 |
. . . . 5
|
32 | | tgbtwnconn1.11 |
. . . . 5
|
33 | 31, 32 | eqtr2d 2657 |
. . . 4
|
34 | | tgbtwnconn1.8 |
. . . . . 6
|
35 | | tgbtwnconn1.9 |
. . . . . 6
|
36 | 34, 35 | eqtr4d 2659 |
. . . . 5
|
37 | 1, 2, 3, 4, 10, 11, 18, 17, 36 | tgcgrcomlr 25375 |
. . . 4
|
38 | 1, 2, 3, 4, 5, 11,
10, 6, 17, 18, 28, 30, 33, 37 | tgcgrextend 25380 |
. . 3
|
39 | | tgbtwnconn1.10 |
. . . 4
|
40 | 1, 2, 3, 4, 10, 8,
5, 18, 39 | tgcgrcomr 25373 |
. . 3
|
41 | 1, 2, 3, 4, 5, 10,
8, 6, 18, 5, 24, 27, 38, 40 | tgcgrextend 25380 |
. 2
|
42 | 1, 2, 3, 4, 5, 6 | axtgcgrrflx 25361 |
. 2
|
43 | 1, 2, 3, 4, 5, 6, 5, 7, 8, 6, 9, 16, 23, 41, 42 | tgsegconeq 25381 |
1
|