Step Hyp Ref
Expression 1 nfv 1707 . . . . . . . 8
2 nfv 1707 . . . . . . . 8
3 nfra1 2838 . . . . . . . 8
4 1 , 2 , 3 nf3an 1930 . . . . . . 7
5 nfv 1707 . . . . . . . 8
6 nfra1 2838 . . . . . . . . 9
7 nfra1 2838 . . . . . . . . 9
8 6 , 7 nfan 1928 . . . . . . . 8
9 5 , 8 nfan 1928 . . . . . . 7
10 4 , 9 nfan 1928 . . . . . 6
11 nfv 1707 . . . . . . . . 9
12 nfv 1707 . . . . . . . . 9
13 nfra2 2844 . . . . . . . . 9
14 11 , 12 , 13 nf3an 1930 . . . . . . . 8
15 nfv 1707 . . . . . . . 8
16 14 , 15 nfan 1928 . . . . . . 7
17 nfv 1707 . . . . . . 7
18 simprrl 765 . . . . . . . . . . . 12
19 18 r19.21bi 2826 . . . . . . . . . . 11
20 simpl2l 1049 . . . . . . . . . . . . 13
21 20 sselda 3503 . . . . . . . . . . . 12
22 simplrl 761 . . . . . . . . . . . 12
23 21 , 22 lenltd 9752 . . . . . . . . . . 11
24 19 , 23 mpbird 232 . . . . . . . . . 10
25 24 ex 434 . . . . . . . . 9
26 simpl3 1001 . . . . . . . . . . . . . . 15
27 simp2 997 . . . . . . . . . . . . . . . 16
28 simpr 461 . . . . . . . . . . . . . . . 16
29 rsp 2823 . . . . . . . . . . . . . . . . . . . . 21
30 29 com12 31 . . . . . . . . . . . . . . . . . . . 20
31 30 adantl 466 . . . . . . . . . . . . . . . . . . 19
32 ssel2 3498 . . . . . . . . . . . . . . . . . . . . . 22
33 32 adantlr 714 . . . . . . . . . . . . . . . . . . . . 21
34 33 adantr 465 . . . . . . . . . . . . . . . . . . . 20
35 simplr 755 . . . . . . . . . . . . . . . . . . . . 21
36 35 sselda 3503 . . . . . . . . . . . . . . . . . . . 20
37 ltnsym 9704 . . . . . . . . . . . . . . . . . . . 20
38 34 , 36 , 37 syl2anc 661 . . . . . . . . . . . . . . . . . . 19
39 31 , 38 syld 44 . . . . . . . . . . . . . . . . . 18
40 39 an32s 804 . . . . . . . . . . . . . . . . 17
41 40 ralimdva 2865 . . . . . . . . . . . . . . . 16
42 27 , 28 , 41 syl2an 477 . . . . . . . . . . . . . . 15
43 26 , 42 mpd 15 . . . . . . . . . . . . . 14
44 breq2 4456 . . . . . . . . . . . . . . . 16
45 44 notbid 294 . . . . . . . . . . . . . . 15
46 45 cbvralv 3084 . . . . . . . . . . . . . 14
47 43 , 46 sylib 196 . . . . . . . . . . . . 13
48 ralnex 2903 . . . . . . . . . . . . 13
49 47 , 48 sylib 196 . . . . . . . . . . . 12
50 simp2r 1023 . . . . . . . . . . . . . 14
51 ssel2 3498 . . . . . . . . . . . . . 14
52 50 , 28 , 51 syl2an 477 . . . . . . . . . . . . 13
53 simplrr 762 . . . . . . . . . . . . . 14
54 53 adantl 466 . . . . . . . . . . . . 13
55 breq1 4455 . . . . . . . . . . . . . . 15
56 breq1 4455 . . . . . . . . . . . . . . . 16
57 56 rexbidv 2968 . . . . . . . . . . . . . . 15
58 55 , 57 imbi12d 320 . . . . . . . . . . . . . 14
59 58 rspcv 3206 . . . . . . . . . . . . 13
60 52 , 54 , 59 sylc 60 . . . . . . . . . . . 12
61 49 , 60 mtod 177 . . . . . . . . . . 11
62 simprll 763 . . . . . . . . . . . 12
63 62 , 52 lenltd 9752 . . . . . . . . . . 11
64 61 , 63 mpbird 232 . . . . . . . . . 10
65 64 expr 615 . . . . . . . . 9
66 25 , 65 anim12d 563 . . . . . . . 8
67 66 expd 436 . . . . . . 7
68 16 , 17 , 67 ralrimd 2861 . . . . . 6
69 10 , 68 ralrimi 2857 . . . . 5
70 simp2l 1022 . . . . . 6
71 simp1l 1020 . . . . . 6
72 simp1r 1021 . . . . . . . . 9
73 n0 3794 . . . . . . . . 9
74 72 , 73 sylib 196 . . . . . . . 8
75 50 sseld 3502 . . . . . . . . . 10
76 ralcom 3018 . . . . . . . . . . . 12
77 breq2 4456 . . . . . . . . . . . . . 14
78 77 ralbidv 2896 . . . . . . . . . . . . 13
79 78 rspccv 3207 . . . . . . . . . . . 12
80 76 , 79 sylbi 195 . . . . . . . . . . 11
81 80 3ad2ant3 1019 . . . . . . . . . 10
82 75 , 81 jcad 533 . . . . . . . . 9
83 82 eximdv 1710 . . . . . . . 8
84 74 , 83 mpd 15 . . . . . . 7
85 df-rex 2813 . . . . . . 7
86 84 , 85 sylibr 212 . . . . . 6
87 axsup 9681 . . . . . 6
88 70 , 71 , 86 , 87 syl3anc 1228 . . . . 5
89 69 , 88 reximddv 2933 . . . 4
90 89 3expib 1199 . . 3
91 1re 9616 . . . . 5
92 rzal 3931 . . . . 5
93 breq2 4456 . . . . . . . 8
94 breq1 4455 . . . . . . . 8
95 93 , 94 anbi12d 710 . . . . . . 7
96 95 2ralbidv 2901 . . . . . 6
97 96 rspcev 3210 . . . . 5
98 91 , 92 , 97 sylancr 663 . . . 4
99 98 a1d 25 . . 3
100 rzal 3931 . . . . . 6
101 100 ralrimivw 2872 . . . . 5
102 91 , 101 , 97 sylancr 663 . . . 4
103 102 a1d 25 . . 3
104 90 , 99 , 103 pm2.61iine 2779 . 2
105 104 3impa 1191 1
