Step | Hyp | Ref
| Expression |
1 | | scutcut 31912 |
. . . . . . . . 9
|
2 | 1 | simp1d 1073 |
. . . . . . . 8
|
3 | 2 | ad3antrrr 766 |
. . . . . . 7
|
4 | | scutcut 31912 |
. . . . . . . . 9
|
5 | 4 | simp1d 1073 |
. . . . . . . 8
|
6 | 5 | ad3antlr 767 |
. . . . . . 7
|
7 | | ssltss2 31904 |
. . . . . . . . 9
|
8 | 7 | ad2antlr 763 |
. . . . . . . 8
|
9 | 8 | sselda 3603 |
. . . . . . 7
|
10 | | simplr 792 |
. . . . . . 7
|
11 | 4 | simp3d 1075 |
. . . . . . . . . . 11
|
12 | 11 | ad2antlr 763 |
. . . . . . . . . 10
|
13 | | ssltsep 31905 |
. . . . . . . . . 10
|
14 | 12, 13 | syl 17 |
. . . . . . . . 9
|
15 | | ovex 6678 |
. . . . . . . . . 10
|
16 | | breq1 4656 |
. . . . . . . . . . 11
|
17 | 16 | ralbidv 2986 |
. . . . . . . . . 10
|
18 | 15, 17 | ralsn 4222 |
. . . . . . . . 9
|
19 | 14, 18 | sylib 208 |
. . . . . . . 8
|
20 | 19 | r19.21bi 2932 |
. . . . . . 7
|
21 | 3, 6, 9, 10, 20 | slelttrd 31886 |
. . . . . 6
|
22 | 21 | ralrimiva 2966 |
. . . . 5
|
23 | | ssltss1 31903 |
. . . . . . . . . 10
|
24 | 23 | adantr 481 |
. . . . . . . . 9
|
25 | 24 | adantr 481 |
. . . . . . . 8
|
26 | 25 | sselda 3603 |
. . . . . . 7
|
27 | 2 | ad3antrrr 766 |
. . . . . . 7
|
28 | 5 | ad3antlr 767 |
. . . . . . 7
|
29 | 1 | simp2d 1074 |
. . . . . . . . . . . 12
|
30 | 29 | adantr 481 |
. . . . . . . . . . 11
|
31 | 30 | adantr 481 |
. . . . . . . . . 10
|
32 | | ssltsep 31905 |
. . . . . . . . . 10
|
33 | 31, 32 | syl 17 |
. . . . . . . . 9
|
34 | 33 | r19.21bi 2932 |
. . . . . . . 8
|
35 | | ovex 6678 |
. . . . . . . . 9
|
36 | | breq2 4657 |
. . . . . . . . 9
|
37 | 35, 36 | ralsn 4222 |
. . . . . . . 8
|
38 | 34, 37 | sylib 208 |
. . . . . . 7
|
39 | | simplr 792 |
. . . . . . 7
|
40 | 26, 27, 28, 38, 39 | sltletrd 31885 |
. . . . . 6
|
41 | 40 | ralrimiva 2966 |
. . . . 5
|
42 | 22, 41 | jca 554 |
. . . 4
|
43 | | bdayelon 31892 |
. . . . . . 7
|
44 | 43 | onordi 5832 |
. . . . . 6
|
45 | | ordn2lp 5743 |
. . . . . 6
|
46 | 44, 45 | ax-mp 5 |
. . . . 5
|
47 | 5 | ad2antlr 763 |
. . . . . . 7
|
48 | 2 | adantr 481 |
. . . . . . . 8
|
49 | 48 | adantr 481 |
. . . . . . 7
|
50 | | sltnle 31878 |
. . . . . . 7
|
51 | 47, 49, 50 | syl2anc 693 |
. . . . . 6
|
52 | 5 | ad3antlr 767 |
. . . . . . . . 9
|
53 | | ssltex1 31901 |
. . . . . . . . . . . 12
|
54 | 53 | ad3antrrr 766 |
. . . . . . . . . . 11
|
55 | | snex 4908 |
. . . . . . . . . . 11
|
56 | 54, 55 | jctir 561 |
. . . . . . . . . 10
|
57 | 23 | ad3antrrr 766 |
. . . . . . . . . . 11
|
58 | 52 | snssd 4340 |
. . . . . . . . . . 11
|
59 | | simplrr 801 |
. . . . . . . . . . . 12
|
60 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
61 | 15, 60 | ralsn 4222 |
. . . . . . . . . . . . 13
|
62 | 61 | ralbii 2980 |
. . . . . . . . . . . 12
|
63 | 59, 62 | sylibr 224 |
. . . . . . . . . . 11
|
64 | 57, 58, 63 | 3jca 1242 |
. . . . . . . . . 10
|
65 | | brsslt 31900 |
. . . . . . . . . 10
|
66 | 56, 64, 65 | sylanbrc 698 |
. . . . . . . . 9
|
67 | | ssltex2 31902 |
. . . . . . . . . . . 12
|
68 | 67 | ad3antrrr 766 |
. . . . . . . . . . 11
|
69 | 68, 55 | jctil 560 |
. . . . . . . . . 10
|
70 | | ssltss2 31904 |
. . . . . . . . . . . 12
|
71 | 70 | ad3antrrr 766 |
. . . . . . . . . . 11
|
72 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
|
73 | 48 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
74 | 71 | sselda 3603 |
. . . . . . . . . . . . . 14
|
75 | | simplr 792 |
. . . . . . . . . . . . . 14
|
76 | 1 | simp3d 1075 |
. . . . . . . . . . . . . . . . . 18
|
77 | 76 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
|
78 | | ssltsep 31905 |
. . . . . . . . . . . . . . . . 17
|
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
|
80 | | breq1 4656 |
. . . . . . . . . . . . . . . . . 18
|
81 | 80 | ralbidv 2986 |
. . . . . . . . . . . . . . . . 17
|
82 | 35, 81 | ralsn 4222 |
. . . . . . . . . . . . . . . 16
|
83 | 79, 82 | sylib 208 |
. . . . . . . . . . . . . . 15
|
84 | 83 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
|
85 | 72, 73, 74, 75, 84 | slttrd 31884 |
. . . . . . . . . . . . 13
|
86 | 85 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
87 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
88 | 87 | ralbidv 2986 |
. . . . . . . . . . . . 13
|
89 | 15, 88 | ralsn 4222 |
. . . . . . . . . . . 12
|
90 | 86, 89 | sylibr 224 |
. . . . . . . . . . 11
|
91 | 58, 71, 90 | 3jca 1242 |
. . . . . . . . . 10
|
92 | | brsslt 31900 |
. . . . . . . . . 10
|
93 | 69, 91, 92 | sylanbrc 698 |
. . . . . . . . 9
|
94 | | sltirr 31871 |
. . . . . . . . . . . . . 14
|
95 | 49, 94 | syl 17 |
. . . . . . . . . . . . 13
|
96 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
97 | 96 | notbid 308 |
. . . . . . . . . . . . 13
|
98 | 95, 97 | syl5ibcom 235 |
. . . . . . . . . . . 12
|
99 | 98 | necon2ad 2809 |
. . . . . . . . . . 11
|
100 | 99 | imp 445 |
. . . . . . . . . 10
|
101 | 100 | necomd 2849 |
. . . . . . . . 9
|
102 | | scutbdaylt 31922 |
. . . . . . . . 9
|
103 | 52, 66, 93, 101, 102 | syl121anc 1331 |
. . . . . . . 8
|
104 | 2 | ad3antrrr 766 |
. . . . . . . . 9
|
105 | | ssltex1 31901 |
. . . . . . . . . . . 12
|
106 | 105 | ad3antlr 767 |
. . . . . . . . . . 11
|
107 | | snex 4908 |
. . . . . . . . . . 11
|
108 | 106, 107 | jctir 561 |
. . . . . . . . . 10
|
109 | | ssltss1 31903 |
. . . . . . . . . . . 12
|
110 | 109 | ad3antlr 767 |
. . . . . . . . . . 11
|
111 | 104 | snssd 4340 |
. . . . . . . . . . 11
|
112 | 110 | sselda 3603 |
. . . . . . . . . . . . . 14
|
113 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
|
114 | 48 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
115 | 4 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | ad3antlr 767 |
. . . . . . . . . . . . . . . . 17
|
117 | | ssltsep 31905 |
. . . . . . . . . . . . . . . . 17
|
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
|
119 | 118 | r19.21bi 2932 |
. . . . . . . . . . . . . . 15
|
120 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
|
121 | 15, 120 | ralsn 4222 |
. . . . . . . . . . . . . . 15
|
122 | 119, 121 | sylib 208 |
. . . . . . . . . . . . . 14
|
123 | | simplr 792 |
. . . . . . . . . . . . . 14
|
124 | 112, 113,
114, 122, 123 | slttrd 31884 |
. . . . . . . . . . . . 13
|
125 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
126 | 35, 125 | ralsn 4222 |
. . . . . . . . . . . . 13
|
127 | 124, 126 | sylibr 224 |
. . . . . . . . . . . 12
|
128 | 127 | ralrimiva 2966 |
. . . . . . . . . . 11
|
129 | 110, 111,
128 | 3jca 1242 |
. . . . . . . . . 10
|
130 | | brsslt 31900 |
. . . . . . . . . 10
|
131 | 108, 129,
130 | sylanbrc 698 |
. . . . . . . . 9
|
132 | | ssltex2 31902 |
. . . . . . . . . . . 12
|
133 | 132 | ad3antlr 767 |
. . . . . . . . . . 11
|
134 | 133, 107 | jctil 560 |
. . . . . . . . . 10
|
135 | 7 | ad3antlr 767 |
. . . . . . . . . . 11
|
136 | | simplrl 800 |
. . . . . . . . . . . 12
|
137 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
138 | 137 | ralbidv 2986 |
. . . . . . . . . . . . 13
|
139 | 35, 138 | ralsn 4222 |
. . . . . . . . . . . 12
|
140 | 136, 139 | sylibr 224 |
. . . . . . . . . . 11
|
141 | 111, 135,
140 | 3jca 1242 |
. . . . . . . . . 10
|
142 | | brsslt 31900 |
. . . . . . . . . 10
|
143 | 134, 141,
142 | sylanbrc 698 |
. . . . . . . . 9
|
144 | | scutbdaylt 31922 |
. . . . . . . . 9
|
145 | 104, 131,
143, 100, 144 | syl121anc 1331 |
. . . . . . . 8
|
146 | 103, 145 | jca 554 |
. . . . . . 7
|
147 | 146 | ex 450 |
. . . . . 6
|
148 | 51, 147 | sylbird 250 |
. . . . 5
|
149 | 46, 148 | mt3i 141 |
. . . 4
|
150 | 42, 149 | impbida 877 |
. . 3
|
151 | | breq12 4658 |
. . . 4
|
152 | | breq1 4656 |
. . . . . 6
|
153 | 152 | ralbidv 2986 |
. . . . 5
|
154 | | breq2 4657 |
. . . . . 6
|
155 | 154 | ralbidv 2986 |
. . . . 5
|
156 | 153, 155 | bi2anan9 917 |
. . . 4
|
157 | 151, 156 | bibi12d 335 |
. . 3
|
158 | 150, 157 | syl5ibr 236 |
. 2
|
159 | 158 | impcom 446 |
1
|