Step | Hyp | Ref
| Expression |
1 | | tgcgrxfr.a |
. . . 4
|
2 | 1 | adantr 481 |
. . 3
|
3 | | tgcgrxfr.p |
. . . 4
|
4 | | tgcgrxfr.m |
. . . 4
|
5 | | tgcgrxfr.i |
. . . 4
Itv |
6 | | tgcgrxfr.g |
. . . . 5
TarskiG |
7 | 6 | adantr 481 |
. . . 4
TarskiG |
8 | | tgcgrxfr.d |
. . . . 5
|
9 | 8 | adantr 481 |
. . . 4
|
10 | | tgcgrxfr.f |
. . . . 5
|
11 | 10 | adantr 481 |
. . . 4
|
12 | | simpr 477 |
. . . 4
|
13 | 3, 4, 5, 7, 2, 9, 11, 12 | tgldim0itv 25399 |
. . 3
|
14 | | tgcgrxfr.r |
. . . 4
cgrG |
15 | | tgcgrxfr.b |
. . . . 5
|
16 | 15 | adantr 481 |
. . . 4
|
17 | | tgcgrxfr.c |
. . . . 5
|
18 | 17 | adantr 481 |
. . . 4
|
19 | 3, 4, 5, 7, 2, 16,
9, 12, 2 | tgldim0cgr 25400 |
. . . 4
|
20 | 3, 4, 5, 7, 16, 18, 2, 12, 11 | tgldim0cgr 25400 |
. . . 4
|
21 | 3, 4, 5, 7, 18, 2,
11, 12, 9 | tgldim0cgr 25400 |
. . . 4
|
22 | 3, 4, 14, 7, 2, 16, 18, 9, 2, 11, 19, 20, 21 | trgcgr 25411 |
. . 3
|
23 | | eleq1 2689 |
. . . . 5
|
24 | | eqidd 2623 |
. . . . . . 7
|
25 | | id 22 |
. . . . . . 7
|
26 | | eqidd 2623 |
. . . . . . 7
|
27 | 24, 25, 26 | s3eqd 13609 |
. . . . . 6
|
28 | 27 | breq2d 4665 |
. . . . 5
|
29 | 23, 28 | anbi12d 747 |
. . . 4
|
30 | 29 | rspcev 3309 |
. . 3
|
31 | 2, 13, 22, 30 | syl12anc 1324 |
. 2
|
32 | 6 | ad3antrrr 766 |
. . . . 5
TarskiG |
33 | | simplr 792 |
. . . . 5
|
34 | 8 | ad3antrrr 766 |
. . . . 5
|
35 | 1 | ad3antrrr 766 |
. . . . 5
|
36 | 15 | ad3antrrr 766 |
. . . . 5
|
37 | 3, 4, 5, 32, 33, 34, 35, 36 | axtgsegcon 25363 |
. . . 4
|
38 | 6 | ad7antr 774 |
. . . . . . . . . 10
TarskiG |
39 | 33 | ad2antrr 762 |
. . . . . . . . . . 11
|
40 | 39 | ad2antrr 762 |
. . . . . . . . . 10
|
41 | 8 | ad7antr 774 |
. . . . . . . . . 10
|
42 | | simplr 792 |
. . . . . . . . . . 11
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . 10
|
44 | | simplr 792 |
. . . . . . . . . 10
|
45 | | simpllr 799 |
. . . . . . . . . . 11
|
46 | 45 | simpld 475 |
. . . . . . . . . 10
|
47 | | simprl 794 |
. . . . . . . . . 10
|
48 | 3, 4, 5, 38, 40, 41, 43, 44, 46, 47 | tgbtwnexch3 25389 |
. . . . . . . . 9
|
49 | 1 | ad7antr 774 |
. . . . . . . . . . 11
|
50 | 17 | ad7antr 774 |
. . . . . . . . . . 11
|
51 | 10 | ad7antr 774 |
. . . . . . . . . . 11
|
52 | | simp-5r 809 |
. . . . . . . . . . . . 13
|
53 | 52 | simprd 479 |
. . . . . . . . . . . 12
|
54 | 53 | necomd 2849 |
. . . . . . . . . . 11
|
55 | 3, 4, 5, 38, 40, 41, 43, 44, 46, 47 | tgbtwnexch 25393 |
. . . . . . . . . . 11
|
56 | 52 | simpld 475 |
. . . . . . . . . . . 12
|
57 | 3, 4, 5, 38, 51, 41, 40, 56 | tgbtwncom 25383 |
. . . . . . . . . . 11
|
58 | 15 | ad7antr 774 |
. . . . . . . . . . . 12
|
59 | | tgcgrxfr.1 |
. . . . . . . . . . . . 13
|
60 | 59 | ad7antr 774 |
. . . . . . . . . . . 12
|
61 | 45 | simprd 479 |
. . . . . . . . . . . 12
|
62 | | simprr 796 |
. . . . . . . . . . . 12
|
63 | 3, 4, 5, 38, 41, 43, 44, 49, 58, 50, 48, 60, 61, 62 | tgcgrextend 25380 |
. . . . . . . . . . 11
|
64 | | tgcgrxfr.2 |
. . . . . . . . . . . . 13
|
65 | 64 | ad7antr 774 |
. . . . . . . . . . . 12
|
66 | 65 | eqcomd 2628 |
. . . . . . . . . . 11
|
67 | 3, 4, 5, 38, 41, 49, 50, 40, 44, 51, 54, 55, 57, 63, 66 | tgsegconeq 25381 |
. . . . . . . . . 10
|
68 | 67 | oveq2d 6666 |
. . . . . . . . 9
|
69 | 48, 68 | eleqtrd 2703 |
. . . . . . . 8
|
70 | 61 | eqcomd 2628 |
. . . . . . . . 9
|
71 | 67 | oveq2d 6666 |
. . . . . . . . . 10
|
72 | 62, 71 | eqtr3d 2658 |
. . . . . . . . 9
|
73 | 3, 4, 5, 6, 1, 17,
8, 10, 64 | tgcgrcomlr 25375 |
. . . . . . . . . 10
|
74 | 73 | ad7antr 774 |
. . . . . . . . 9
|
75 | 3, 4, 14, 38, 49, 58, 50, 41, 43, 51, 70, 72, 74 | trgcgr 25411 |
. . . . . . . 8
|
76 | 69, 75 | jca 554 |
. . . . . . 7
|
77 | 32 | ad2antrr 762 |
. . . . . . . 8
TarskiG |
78 | 36 | ad2antrr 762 |
. . . . . . . 8
|
79 | 17 | ad5antr 770 |
. . . . . . . 8
|
80 | 3, 4, 5, 77, 39, 42, 78, 79 | axtgsegcon 25363 |
. . . . . . 7
|
81 | 76, 80 | r19.29a 3078 |
. . . . . 6
|
82 | 81 | ex 450 |
. . . . 5
|
83 | 82 | reximdva 3017 |
. . . 4
|
84 | 37, 83 | mpd 15 |
. . 3
|
85 | 6 | adantr 481 |
. . . 4
TarskiG |
86 | 10 | adantr 481 |
. . . 4
|
87 | 8 | adantr 481 |
. . . 4
|
88 | | simpr 477 |
. . . 4
|
89 | 3, 4, 5, 85, 86, 87, 88 | tgbtwndiff 25401 |
. . 3
|
90 | 84, 89 | r19.29a 3078 |
. 2
|
91 | 3, 1 | tgldimor 25397 |
. 2
|
92 | 31, 90, 91 | mpjaodan 827 |
1
|