Step | Hyp | Ref
| Expression |
1 | | neirr 2803 |
. . . . . . 7
|
2 | 1 | intnan 960 |
. . . . . 6
|
3 | | legval.p |
. . . . . . 7
|
4 | | legval.d |
. . . . . . 7
|
5 | | legval.i |
. . . . . . 7
Itv |
6 | | legval.l |
. . . . . . 7
≤G |
7 | | legval.g |
. . . . . . . . 9
TarskiG |
8 | 7 | adantr 481 |
. . . . . . . 8
TarskiG |
9 | 8 | ad3antrrr 766 |
. . . . . . 7
TarskiG |
10 | | legso.a |
. . . . . . 7
|
11 | | legso.f |
. . . . . . . . 9
|
12 | 11 | adantr 481 |
. . . . . . . 8
|
13 | 12 | ad3antrrr 766 |
. . . . . . 7
|
14 | | legso.l |
. . . . . . 7
|
15 | | legso.d |
. . . . . . . 8
|
16 | 15 | ad4antr 768 |
. . . . . . 7
|
17 | | simpllr 799 |
. . . . . . 7
|
18 | | simplr 792 |
. . . . . . 7
|
19 | 3, 4, 5, 6, 9, 10,
13, 14, 16, 17, 18 | ltgov 25492 |
. . . . . 6
|
20 | 2, 19 | mtbiri 317 |
. . . . 5
|
21 | | simpr 477 |
. . . . . 6
|
22 | 21, 21 | breq12d 4666 |
. . . . 5
|
23 | 20, 22 | mtbird 315 |
. . . 4
|
24 | | simpr 477 |
. . . . 5
|
25 | 3, 4, 5, 6, 8, 10,
12, 24 | ltgseg 25491 |
. . . 4
|
26 | 23, 25 | r19.29vva 3081 |
. . 3
|
27 | 7 | ad8antr 776 |
. . . . . . . . . . 11
TarskiG |
28 | 27 | ad3antrrr 766 |
. . . . . . . . . 10
TarskiG |
29 | | simp-9r 817 |
. . . . . . . . . 10
|
30 | | simp-8r 815 |
. . . . . . . . . 10
|
31 | | simp-6r 811 |
. . . . . . . . . 10
|
32 | | simp-5r 809 |
. . . . . . . . . 10
|
33 | | simpllr 799 |
. . . . . . . . . 10
|
34 | | simplr 792 |
. . . . . . . . . 10
|
35 | | simp-10r 819 |
. . . . . . . . . . . . . 14
|
36 | 35 | simpld 475 |
. . . . . . . . . . . . 13
|
37 | | simp-7r 813 |
. . . . . . . . . . . . 13
|
38 | | simp-4r 807 |
. . . . . . . . . . . . 13
|
39 | 36, 37, 38 | 3brtr3d 4684 |
. . . . . . . . . . . 12
|
40 | 11 | ad8antr 776 |
. . . . . . . . . . . . . 14
|
41 | 40 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
42 | 15 | ad8antr 776 |
. . . . . . . . . . . . . 14
|
43 | 42 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
44 | 3, 4, 5, 6, 28, 10, 41, 14, 43, 29, 30 | ltgov 25492 |
. . . . . . . . . . . 12
|
45 | 39, 44 | mpbid 222 |
. . . . . . . . . . 11
|
46 | 45 | simpld 475 |
. . . . . . . . . 10
|
47 | 35 | simprd 479 |
. . . . . . . . . . . . 13
|
48 | | simpr 477 |
. . . . . . . . . . . . 13
|
49 | 47, 38, 48 | 3brtr3d 4684 |
. . . . . . . . . . . 12
|
50 | 3, 4, 5, 6, 28, 10, 41, 14, 43, 31, 32 | ltgov 25492 |
. . . . . . . . . . . 12
|
51 | 49, 50 | mpbid 222 |
. . . . . . . . . . 11
|
52 | 51 | simpld 475 |
. . . . . . . . . 10
|
53 | 3, 4, 5, 6, 28, 29, 30, 31, 32, 33, 34, 46, 52 | legtrd 25484 |
. . . . . . . . 9
|
54 | 28 | adantr 481 |
. . . . . . . . . . . 12
TarskiG |
55 | 29 | adantr 481 |
. . . . . . . . . . . 12
|
56 | 30 | adantr 481 |
. . . . . . . . . . . 12
|
57 | 31 | adantr 481 |
. . . . . . . . . . . 12
|
58 | 32 | adantr 481 |
. . . . . . . . . . . 12
|
59 | 46 | adantr 481 |
. . . . . . . . . . . 12
|
60 | 52 | adantr 481 |
. . . . . . . . . . . . 13
|
61 | | simpr 477 |
. . . . . . . . . . . . 13
|
62 | 60, 61 | breqtrrd 4681 |
. . . . . . . . . . . 12
|
63 | 3, 4, 5, 6, 54, 55, 56, 57, 58, 59, 62 | legtri3 25485 |
. . . . . . . . . . 11
|
64 | 45 | simprd 479 |
. . . . . . . . . . . . 13
|
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
|
66 | 65 | neneqd 2799 |
. . . . . . . . . . 11
|
67 | 63, 66 | pm2.65da 600 |
. . . . . . . . . 10
|
68 | 67 | neqned 2801 |
. . . . . . . . 9
|
69 | 3, 4, 5, 6, 28, 10, 41, 14, 43, 29, 30 | ltgov 25492 |
. . . . . . . . 9
|
70 | 53, 68, 69 | mpbir2and 957 |
. . . . . . . 8
|
71 | 70, 37, 48 | 3brtr4d 4685 |
. . . . . . 7
|
72 | | simp-5r 809 |
. . . . . . . . . 10
|
73 | 72 | simp3d 1075 |
. . . . . . . . 9
|
74 | 73 | ad3antrrr 766 |
. . . . . . . 8
|
75 | 3, 4, 5, 6, 27, 10, 40, 74 | ltgseg 25491 |
. . . . . . 7
|
76 | 71, 75 | r19.29vva 3081 |
. . . . . 6
|
77 | 7 | ad5antr 770 |
. . . . . . 7
TarskiG |
78 | 11 | ad5antr 770 |
. . . . . . 7
|
79 | 72 | simp2d 1074 |
. . . . . . 7
|
80 | 3, 4, 5, 6, 77, 10, 78, 79 | ltgseg 25491 |
. . . . . 6
|
81 | 76, 80 | r19.29vva 3081 |
. . . . 5
|
82 | 7 | ad2antrr 762 |
. . . . . 6
TarskiG |
83 | 11 | ad2antrr 762 |
. . . . . 6
|
84 | | simplr1 1103 |
. . . . . 6
|
85 | 3, 4, 5, 6, 82, 10, 83, 84 | ltgseg 25491 |
. . . . 5
|
86 | 81, 85 | r19.29vva 3081 |
. . . 4
|
87 | 86 | ex 450 |
. . 3
|
88 | 26, 87 | ispod 5043 |
. 2
|
89 | 7 | ad8antr 776 |
. . . . . . . . 9
TarskiG |
90 | | simp-6r 811 |
. . . . . . . . 9
|
91 | | simp-5r 809 |
. . . . . . . . 9
|
92 | | simpllr 799 |
. . . . . . . . 9
|
93 | | simplr 792 |
. . . . . . . . 9
|
94 | 3, 4, 5, 6, 89, 90, 91, 92, 93 | legtrid 25486 |
. . . . . . . 8
|
95 | 11 | ad8antr 776 |
. . . . . . . . . 10
|
96 | 15 | ad8antr 776 |
. . . . . . . . . 10
|
97 | 3, 4, 5, 6, 89, 10, 95, 14, 96, 90, 91 | legov3 25493 |
. . . . . . . . 9
|
98 | 3, 4, 5, 6, 89, 10, 95, 14, 96, 92, 93 | legov3 25493 |
. . . . . . . . 9
|
99 | 97, 98 | orbi12d 746 |
. . . . . . . 8
|
100 | 94, 99 | mpbid 222 |
. . . . . . 7
|
101 | | eqcom 2629 |
. . . . . . . . . 10
|
102 | 101 | orbi2i 541 |
. . . . . . . . 9
|
103 | 102 | orbi2i 541 |
. . . . . . . 8
|
104 | | df-3or 1038 |
. . . . . . . . 9
|
105 | | 3orcomb 1048 |
. . . . . . . . 9
|
106 | | orordir 553 |
. . . . . . . . 9
|
107 | 104, 105,
106 | 3bitr3ri 291 |
. . . . . . . 8
|
108 | 103, 107 | bitr3i 266 |
. . . . . . 7
|
109 | 100, 108 | sylib 208 |
. . . . . 6
|
110 | | simp-4r 807 |
. . . . . . . 8
|
111 | | simpr 477 |
. . . . . . . 8
|
112 | 110, 111 | breq12d 4666 |
. . . . . . 7
|
113 | 110, 111 | eqeq12d 2637 |
. . . . . . 7
|
114 | 111, 110 | breq12d 4666 |
. . . . . . 7
|
115 | 112, 113,
114 | 3orbi123d 1398 |
. . . . . 6
|
116 | 109, 115 | mpbird 247 |
. . . . 5
|
117 | 7 | ad2antrr 762 |
. . . . . . 7
TarskiG |
118 | 11 | ad2antrr 762 |
. . . . . . 7
|
119 | | simpr 477 |
. . . . . . 7
|
120 | 3, 4, 5, 6, 117, 10, 118, 119 | ltgseg 25491 |
. . . . . 6
|
121 | 120 | ad3antrrr 766 |
. . . . 5
|
122 | 116, 121 | r19.29vva 3081 |
. . . 4
|
123 | 25 | adantr 481 |
. . . 4
|
124 | 122, 123 | r19.29vva 3081 |
. . 3
|
125 | 124 | anasss 679 |
. 2
|
126 | 88, 125 | issod 5065 |
1
|