Proof of Theorem tglineeltr
Step | Hyp | Ref
| Expression |
1 | | tglineeltr.7 |
. . . 4
|
2 | | tglineelsb2.p |
. . . . . . 7
|
3 | | tglineelsb2.l |
. . . . . . 7
LineG |
4 | | tglineelsb2.i |
. . . . . . 7
Itv |
5 | | tglineelsb2.g |
. . . . . . . 8
TarskiG |
6 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
7 | | tglineelsb2.1 |
. . . . . . . 8
|
8 | 7 | ad3antrrr 766 |
. . . . . . 7
|
9 | | tglineelsb2.2 |
. . . . . . . 8
|
10 | 9 | ad3antrrr 766 |
. . . . . . 7
|
11 | | simpllr 799 |
. . . . . . 7
|
12 | | eqid 2622 |
. . . . . . . 8
|
13 | | tglineelsb2.3 |
. . . . . . . . 9
|
14 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
15 | | simplr 792 |
. . . . . . . 8
|
16 | | simpr 477 |
. . . . . . . 8
|
17 | 2, 12, 4, 6, 8, 11,
14, 10, 15, 16 | tgbtwnexch 25393 |
. . . . . . 7
|
18 | 2, 3, 4, 6, 8, 10,
11, 17 | btwncolg1 25450 |
. . . . . 6
|
19 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
20 | 7 | ad3antrrr 766 |
. . . . . . 7
|
21 | 9 | ad3antrrr 766 |
. . . . . . 7
|
22 | | simpllr 799 |
. . . . . . 7
|
23 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
24 | | simplr 792 |
. . . . . . . . 9
|
25 | 2, 12, 4, 19, 20, 22, 23, 24 | tgbtwncom 25383 |
. . . . . . . 8
|
26 | | simpr 477 |
. . . . . . . 8
|
27 | 2, 12, 4, 19, 23, 22, 20, 21, 25, 26 | tgbtwnexch3 25389 |
. . . . . . 7
|
28 | 2, 3, 4, 19, 20, 21, 22, 27 | btwncolg2 25451 |
. . . . . 6
|
29 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
30 | 7 | ad3antrrr 766 |
. . . . . . 7
|
31 | | simpllr 799 |
. . . . . . 7
|
32 | 9 | ad3antrrr 766 |
. . . . . . 7
|
33 | 13 | ad3antrrr 766 |
. . . . . . 7
|
34 | | simplr 792 |
. . . . . . 7
|
35 | | simpr 477 |
. . . . . . 7
|
36 | 2, 4, 29, 30, 31, 32, 33, 34, 35, 3 | tgbtwnconnln3 25473 |
. . . . . 6
|
37 | | tglineelsb2.6 |
. . . . . . . 8
|
38 | | tglineelsb2.4 |
. . . . . . . . 9
|
39 | 2, 3, 4, 5, 7, 9, 38, 13 | tgellng 25448 |
. . . . . . . 8
|
40 | 37, 39 | mpbid 222 |
. . . . . . 7
|
41 | 40 | ad2antrr 762 |
. . . . . 6
|
42 | 18, 28, 36, 41 | mpjao3dan 1395 |
. . . . 5
|
43 | 42 | an32s 846 |
. . . 4
|
44 | 1, 43 | mpidan 704 |
. . 3
|
45 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
46 | 7 | ad3antrrr 766 |
. . . . . . 7
|
47 | 9 | ad3antrrr 766 |
. . . . . . 7
|
48 | | simpllr 799 |
. . . . . . 7
|
49 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
50 | | tglineelsb2.5 |
. . . . . . . . . 10
|
51 | 50 | necomd 2849 |
. . . . . . . . 9
|
52 | 51 | ad3antrrr 766 |
. . . . . . . 8
|
53 | | simplr 792 |
. . . . . . . 8
|
54 | | simpr 477 |
. . . . . . . 8
|
55 | 2, 12, 4, 45, 48, 46, 49, 47, 52, 53, 54 | tgbtwnouttr 25392 |
. . . . . . 7
|
56 | 2, 3, 4, 45, 46, 47, 48, 55 | btwncolg2 25451 |
. . . . . 6
|
57 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
58 | 9 | ad3antrrr 766 |
. . . . . . 7
|
59 | | simpllr 799 |
. . . . . . 7
|
60 | 7 | ad3antrrr 766 |
. . . . . . 7
|
61 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
62 | 50 | ad3antrrr 766 |
. . . . . . . 8
|
63 | | simpr 477 |
. . . . . . . 8
|
64 | | simplr 792 |
. . . . . . . . 9
|
65 | 2, 12, 4, 57, 59, 60, 61, 64 | tgbtwncom 25383 |
. . . . . . . 8
|
66 | 2, 4, 57, 61, 60, 58, 59, 3, 62, 63, 65 | tgbtwnconnln2 25476 |
. . . . . . 7
|
67 | 2, 3, 4, 57, 58, 59, 60, 66 | colrot2 25455 |
. . . . . 6
|
68 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
69 | 9 | ad3antrrr 766 |
. . . . . . 7
|
70 | 7 | ad3antrrr 766 |
. . . . . . 7
|
71 | | simpllr 799 |
. . . . . . 7
|
72 | 13 | ad3antrrr 766 |
. . . . . . . . 9
|
73 | | simpr 477 |
. . . . . . . . 9
|
74 | | simplr 792 |
. . . . . . . . 9
|
75 | 2, 12, 4, 68, 69, 70, 71, 72, 73, 74 | tgbtwnintr 25388 |
. . . . . . . 8
|
76 | 2, 3, 4, 68, 69, 70, 71, 75 | btwncolg3 25452 |
. . . . . . 7
|
77 | 2, 3, 4, 68, 69, 70, 71, 76 | colcom 25453 |
. . . . . 6
|
78 | 40 | ad2antrr 762 |
. . . . . 6
|
79 | 56, 67, 77, 78 | mpjao3dan 1395 |
. . . . 5
|
80 | 79 | an32s 846 |
. . . 4
|
81 | 1, 80 | mpidan 704 |
. . 3
|
82 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
83 | 9 | ad3antrrr 766 |
. . . . . . 7
|
84 | | simpllr 799 |
. . . . . . 7
|
85 | 7 | ad3antrrr 766 |
. . . . . . 7
|
86 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
87 | 51 | ad3antrrr 766 |
. . . . . . . 8
|
88 | | simpr 477 |
. . . . . . . 8
|
89 | | simplr 792 |
. . . . . . . 8
|
90 | 2, 4, 82, 85, 86, 83, 84, 3, 87, 88, 89 | tgbtwnconnln1 25475 |
. . . . . . 7
|
91 | 2, 3, 4, 82, 83, 84, 85, 90 | colrot2 25455 |
. . . . . 6
|
92 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
93 | 7 | ad3antrrr 766 |
. . . . . . 7
|
94 | 9 | ad3antrrr 766 |
. . . . . . 7
|
95 | | simpllr 799 |
. . . . . . 7
|
96 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
97 | 50 | ad3antrrr 766 |
. . . . . . . 8
|
98 | | simplr 792 |
. . . . . . . . 9
|
99 | 2, 12, 4, 92, 93, 96, 95, 98 | tgbtwncom 25383 |
. . . . . . . 8
|
100 | | simpr 477 |
. . . . . . . 8
|
101 | 2, 12, 4, 92, 95, 96, 93, 94, 97, 99, 100 | tgbtwnouttr2 25390 |
. . . . . . 7
|
102 | 2, 3, 4, 92, 93, 94, 95, 101 | btwncolg2 25451 |
. . . . . 6
|
103 | 5 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
104 | 7 | ad3antrrr 766 |
. . . . . . 7
|
105 | 9 | ad3antrrr 766 |
. . . . . . 7
|
106 | | simpllr 799 |
. . . . . . 7
|
107 | 13 | ad3antrrr 766 |
. . . . . . . 8
|
108 | | simpr 477 |
. . . . . . . 8
|
109 | | simplr 792 |
. . . . . . . 8
|
110 | 2, 12, 4, 103, 104, 105, 107, 106, 108, 109 | tgbtwnexch 25393 |
. . . . . . 7
|
111 | 2, 3, 4, 103, 104, 105, 106, 110 | btwncolg3 25452 |
. . . . . 6
|
112 | 40 | ad2antrr 762 |
. . . . . 6
|
113 | 91, 102, 111, 112 | mpjao3dan 1395 |
. . . . 5
|
114 | 113 | an32s 846 |
. . . 4
|
115 | 1, 114 | mpidan 704 |
. . 3
|
116 | | id 22 |
. . . 4
|
117 | | tglineeltr.8 |
. . . 4
|
118 | 5 | adantr 481 |
. . . . . 6
TarskiG |
119 | 7 | adantr 481 |
. . . . . 6
|
120 | 13 | adantr 481 |
. . . . . 6
|
121 | 51 | adantr 481 |
. . . . . 6
|
122 | | simpr 477 |
. . . . . 6
|
123 | 2, 3, 4, 118, 119, 120, 121, 122 | tgellng 25448 |
. . . . 5
|
124 | 123 | biimpa 501 |
. . . 4
|
125 | 116, 1, 117, 124 | syl21anc 1325 |
. . 3
|
126 | 44, 81, 115, 125 | mpjao3dan 1395 |
. 2
|
127 | 38 | neneqd 2799 |
. 2
|
128 | | pm5.61 749 |
. . 3
|
129 | 128 | simplbi 476 |
. 2
|
130 | 126, 127,
129 | syl2anc 693 |
1
|