Step | Hyp | Ref
| Expression |
1 | | legval.p |
. . . . 5
|
2 | | legval.d |
. . . . 5
|
3 | | legval.i |
. . . . 5
Itv |
4 | | legval.l |
. . . . 5
≤G |
5 | | legval.g |
. . . . 5
TarskiG |
6 | 1, 2, 3, 4, 5 | legval 25479 |
. . . 4
|
7 | 6 | breqd 4664 |
. . 3
|
8 | | ovex 6678 |
. . . 4
|
9 | | ovex 6678 |
. . . 4
|
10 | | simpr 477 |
. . . . . . 7
|
11 | 10 | eqeq1d 2624 |
. . . . . 6
|
12 | | simpl 473 |
. . . . . . . . 9
|
13 | 12 | eqeq1d 2624 |
. . . . . . . 8
|
14 | 13 | anbi2d 740 |
. . . . . . 7
|
15 | 14 | rexbidv 3052 |
. . . . . 6
|
16 | 11, 15 | anbi12d 747 |
. . . . 5
|
17 | 16 | 2rexbidv 3057 |
. . . 4
|
18 | | eqid 2622 |
. . . 4
|
19 | 8, 9, 17, 18 | braba 4992 |
. . 3
|
20 | 7, 19 | syl6bb 276 |
. 2
|
21 | | anass 681 |
. . . . . . . 8
|
22 | 21 | anbi1i 731 |
. . . . . . 7
|
23 | | eqid 2622 |
. . . . . . . . . . 11
cgrG cgrG |
24 | 5 | ad5antr 770 |
. . . . . . . . . . . 12
TarskiG |
25 | 24 | adantr 481 |
. . . . . . . . . . 11
cgrG TarskiG |
26 | | simp-5r 809 |
. . . . . . . . . . . 12
|
27 | 26 | adantr 481 |
. . . . . . . . . . 11
cgrG |
28 | | simpllr 799 |
. . . . . . . . . . 11
cgrG |
29 | | simp-4r 807 |
. . . . . . . . . . . 12
|
30 | 29 | adantr 481 |
. . . . . . . . . . 11
cgrG |
31 | | legov.c |
. . . . . . . . . . . . 13
|
32 | 31 | ad5antr 770 |
. . . . . . . . . . . 12
|
33 | 32 | adantr 481 |
. . . . . . . . . . 11
cgrG |
34 | | simprl 794 |
. . . . . . . . . . 11
cgrG |
35 | | legov.d |
. . . . . . . . . . . . 13
|
36 | 35 | ad5antr 770 |
. . . . . . . . . . . 12
|
37 | 36 | adantr 481 |
. . . . . . . . . . 11
cgrG |
38 | | simprr 796 |
. . . . . . . . . . . 12
cgrG cgrG |
39 | 1, 2, 3, 23, 25, 27, 30, 28, 33, 37, 34, 38 | cgr3swap23 25419 |
. . . . . . . . . . 11
cgrG cgrG |
40 | | simprl 794 |
. . . . . . . . . . . 12
|
41 | 40 | adantr 481 |
. . . . . . . . . . 11
cgrG |
42 | 1, 2, 3, 23, 25, 27, 28, 30, 33, 34, 37, 39, 41 | tgbtwnxfr 25425 |
. . . . . . . . . 10
cgrG |
43 | | simplrr 801 |
. . . . . . . . . . 11
cgrG |
44 | 1, 2, 3, 23, 25, 27, 28, 30, 33, 34, 37, 39 | cgr3simp1 25415 |
. . . . . . . . . . 11
cgrG |
45 | 43, 44 | eqtrd 2656 |
. . . . . . . . . 10
cgrG |
46 | 42, 45 | jca 554 |
. . . . . . . . 9
cgrG |
47 | | eqid 2622 |
. . . . . . . . . 10
LineG LineG |
48 | | simplr 792 |
. . . . . . . . . 10
|
49 | 1, 47, 3, 24, 26, 48, 29, 40 | btwncolg3 25452 |
. . . . . . . . . 10
LineG |
50 | | simpllr 799 |
. . . . . . . . . . 11
|
51 | 50 | eqcomd 2628 |
. . . . . . . . . 10
|
52 | 1, 47, 3, 24, 26, 29, 48, 23, 32, 36, 2, 49, 51 | lnext 25462 |
. . . . . . . . 9
cgrG |
53 | 46, 52 | reximddv 3018 |
. . . . . . . 8
|
54 | 53 | adantllr 755 |
. . . . . . 7
|
55 | 22, 54 | sylanbr 490 |
. . . . . 6
|
56 | | simprr 796 |
. . . . . . 7
|
57 | | eleq1 2689 |
. . . . . . . . 9
|
58 | | oveq2 6658 |
. . . . . . . . . 10
|
59 | 58 | eqeq2d 2632 |
. . . . . . . . 9
|
60 | 57, 59 | anbi12d 747 |
. . . . . . . 8
|
61 | 60 | cbvrexv 3172 |
. . . . . . 7
|
62 | 56, 61 | sylibr 224 |
. . . . . 6
|
63 | 55, 62 | r19.29a 3078 |
. . . . 5
|
64 | 63 | adantl3r 786 |
. . . 4
|
65 | | simpr 477 |
. . . . 5
|
66 | | oveq1 6657 |
. . . . . . . 8
|
67 | 66 | eqeq2d 2632 |
. . . . . . 7
|
68 | | oveq1 6657 |
. . . . . . . . . 10
|
69 | 68 | eleq2d 2687 |
. . . . . . . . 9
|
70 | | oveq1 6657 |
. . . . . . . . . 10
|
71 | 70 | eqeq2d 2632 |
. . . . . . . . 9
|
72 | 69, 71 | anbi12d 747 |
. . . . . . . 8
|
73 | 72 | rexbidv 3052 |
. . . . . . 7
|
74 | 67, 73 | anbi12d 747 |
. . . . . 6
|
75 | | oveq2 6658 |
. . . . . . . 8
|
76 | 75 | eqeq2d 2632 |
. . . . . . 7
|
77 | | oveq2 6658 |
. . . . . . . . . 10
|
78 | 77 | eleq2d 2687 |
. . . . . . . . 9
|
79 | 78 | anbi1d 741 |
. . . . . . . 8
|
80 | 79 | rexbidv 3052 |
. . . . . . 7
|
81 | 76, 80 | anbi12d 747 |
. . . . . 6
|
82 | 74, 81 | cbvrex2v 3180 |
. . . . 5
|
83 | 65, 82 | sylibr 224 |
. . . 4
|
84 | 64, 83 | r19.29vva 3081 |
. . 3
|
85 | 31 | adantr 481 |
. . . 4
|
86 | 35 | adantr 481 |
. . . 4
|
87 | | eqidd 2623 |
. . . 4
|
88 | | simpr 477 |
. . . 4
|
89 | | oveq1 6657 |
. . . . . . 7
|
90 | 89 | eqeq2d 2632 |
. . . . . 6
|
91 | | oveq1 6657 |
. . . . . . . . 9
|
92 | 91 | eleq2d 2687 |
. . . . . . . 8
|
93 | | oveq1 6657 |
. . . . . . . . 9
|
94 | 93 | eqeq2d 2632 |
. . . . . . . 8
|
95 | 92, 94 | anbi12d 747 |
. . . . . . 7
|
96 | 95 | rexbidv 3052 |
. . . . . 6
|
97 | 90, 96 | anbi12d 747 |
. . . . 5
|
98 | | oveq2 6658 |
. . . . . . 7
|
99 | 98 | eqeq2d 2632 |
. . . . . 6
|
100 | | oveq2 6658 |
. . . . . . . . 9
|
101 | 100 | eleq2d 2687 |
. . . . . . . 8
|
102 | 101 | anbi1d 741 |
. . . . . . 7
|
103 | 102 | rexbidv 3052 |
. . . . . 6
|
104 | 99, 103 | anbi12d 747 |
. . . . 5
|
105 | 97, 104 | rspc2ev 3324 |
. . . 4
|
106 | 85, 86, 87, 88, 105 | syl112anc 1330 |
. . 3
|
107 | 84, 106 | impbida 877 |
. 2
|
108 | 20, 107 | bitrd 268 |
1
|