Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . . . . . . 8
|
2 | | nfv 1843 |
. . . . . . . 8
|
3 | | nfra1 2941 |
. . . . . . . 8
|
4 | 1, 2, 3 | nf3an 1831 |
. . . . . . 7
|
5 | | nfv 1843 |
. . . . . . . 8
|
6 | | nfra1 2941 |
. . . . . . . . 9
|
7 | | nfra1 2941 |
. . . . . . . . 9
|
8 | 6, 7 | nfan 1828 |
. . . . . . . 8
|
9 | 5, 8 | nfan 1828 |
. . . . . . 7
|
10 | 4, 9 | nfan 1828 |
. . . . . 6
|
11 | | nfv 1843 |
. . . . . . . . 9
|
12 | | nfv 1843 |
. . . . . . . . 9
|
13 | | nfra2 2946 |
. . . . . . . . 9
|
14 | 11, 12, 13 | nf3an 1831 |
. . . . . . . 8
|
15 | | nfv 1843 |
. . . . . . . 8
|
16 | 14, 15 | nfan 1828 |
. . . . . . 7
|
17 | | nfv 1843 |
. . . . . . 7
|
18 | | simprrl 804 |
. . . . . . . . . . . 12
|
19 | 18 | r19.21bi 2932 |
. . . . . . . . . . 11
|
20 | | simpl2l 1114 |
. . . . . . . . . . . . 13
|
21 | 20 | sselda 3603 |
. . . . . . . . . . . 12
|
22 | | simplrl 800 |
. . . . . . . . . . . 12
|
23 | 21, 22 | lenltd 10183 |
. . . . . . . . . . 11
|
24 | 19, 23 | mpbird 247 |
. . . . . . . . . 10
|
25 | 24 | ex 450 |
. . . . . . . . 9
|
26 | | simpl3 1066 |
. . . . . . . . . . . . . . 15
|
27 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
|
28 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
29 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | ssel2 3598 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 32 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | ltnsym 10135 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 34, 36, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 31, 38 | syld 47 |
. . . . . . . . . . . . . . . . . 18
|
40 | 39 | an32s 846 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | ralimdva 2962 |
. . . . . . . . . . . . . . . 16
|
42 | 27, 28, 41 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
43 | 26, 42 | mpd 15 |
. . . . . . . . . . . . . 14
|
44 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | notbid 308 |
. . . . . . . . . . . . . . 15
|
46 | 45 | cbvralv 3171 |
. . . . . . . . . . . . . 14
|
47 | 43, 46 | sylib 208 |
. . . . . . . . . . . . 13
|
48 | | ralnex 2992 |
. . . . . . . . . . . . 13
|
49 | 47, 48 | sylib 208 |
. . . . . . . . . . . 12
|
50 | | simp2r 1088 |
. . . . . . . . . . . . . 14
|
51 | | ssel2 3598 |
. . . . . . . . . . . . . 14
|
52 | 50, 28, 51 | syl2an 494 |
. . . . . . . . . . . . 13
|
53 | | simplrr 801 |
. . . . . . . . . . . . . 14
|
54 | 53 | adantl 482 |
. . . . . . . . . . . . 13
|
55 | | breq1 4656 |
. . . . . . . . . . . . . . 15
|
56 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
|
58 | 55, 57 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
59 | 58 | rspcv 3305 |
. . . . . . . . . . . . 13
|
60 | 52, 54, 59 | sylc 65 |
. . . . . . . . . . . 12
|
61 | 49, 60 | mtod 189 |
. . . . . . . . . . 11
|
62 | | simprll 802 |
. . . . . . . . . . . 12
|
63 | 62, 52 | lenltd 10183 |
. . . . . . . . . . 11
|
64 | 61, 63 | mpbird 247 |
. . . . . . . . . 10
|
65 | 64 | expr 643 |
. . . . . . . . 9
|
66 | 25, 65 | anim12d 586 |
. . . . . . . 8
|
67 | 66 | expd 452 |
. . . . . . 7
|
68 | 16, 17, 67 | ralrimd 2959 |
. . . . . 6
|
69 | 10, 68 | ralrimi 2957 |
. . . . 5
|
70 | | simp2l 1087 |
. . . . . 6
|
71 | | simp1l 1085 |
. . . . . 6
|
72 | | simp1r 1086 |
. . . . . . . . 9
|
73 | | n0 3931 |
. . . . . . . . 9
|
74 | 72, 73 | sylib 208 |
. . . . . . . 8
|
75 | 50 | sseld 3602 |
. . . . . . . . . 10
|
76 | | ralcom 3098 |
. . . . . . . . . . . 12
|
77 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
78 | 77 | ralbidv 2986 |
. . . . . . . . . . . . 13
|
79 | 78 | rspccv 3306 |
. . . . . . . . . . . 12
|
80 | 76, 79 | sylbi 207 |
. . . . . . . . . . 11
|
81 | 80 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
82 | 75, 81 | jcad 555 |
. . . . . . . . 9
|
83 | 82 | eximdv 1846 |
. . . . . . . 8
|
84 | 74, 83 | mpd 15 |
. . . . . . 7
|
85 | | df-rex 2918 |
. . . . . . 7
|
86 | 84, 85 | sylibr 224 |
. . . . . 6
|
87 | | axsup 10113 |
. . . . . 6
|
88 | 70, 71, 86, 87 | syl3anc 1326 |
. . . . 5
|
89 | 69, 88 | reximddv 3018 |
. . . 4
|
90 | 89 | 3expib 1268 |
. . 3
|
91 | | 1re 10039 |
. . . . 5
|
92 | | rzal 4073 |
. . . . 5
|
93 | | breq2 4657 |
. . . . . . . 8
|
94 | | breq1 4656 |
. . . . . . . 8
|
95 | 93, 94 | anbi12d 747 |
. . . . . . 7
|
96 | 95 | 2ralbidv 2989 |
. . . . . 6
|
97 | 96 | rspcev 3309 |
. . . . 5
|
98 | 91, 92, 97 | sylancr 695 |
. . . 4
|
99 | 98 | a1d 25 |
. . 3
|
100 | | rzal 4073 |
. . . . . 6
|
101 | 100 | ralrimivw 2967 |
. . . . 5
|
102 | 91, 101, 97 | sylancr 695 |
. . . 4
|
103 | 102 | a1d 25 |
. . 3
|
104 | 90, 99, 103 | pm2.61iine 2884 |
. 2
|
105 | 104 | 3impa 1259 |
1
|