Step Hyp Ref
Expression
1 f1ofo 5828
. . . 4
2 df-fo 5599
. . . . 5
3 freq2 4855
. . . . . . 7
4 3 biimprd 223
. . . . . 6
5 df-fn 5596
. . . . . . 7
6 df-fr 4843
. . . . . . . . . . . . . . . . . . . 20
7 vex 3112
. . . . . . . . . . . . . . . . . . . . . 22
8 7 funimaex 5671
. . . . . . . . . . . . . . . . . . . . 21
9 n0 3794
. . . . . . . . . . . . . . . . . . . . . . . . 25
10 funfvima2 6148
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
11 ne0i 3790
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
12 10 , 11 syl6 33
. . . . . . . . . . . . . . . . . . . . . . . . . 26
13 12 exlimdv 1724
. . . . . . . . . . . . . . . . . . . . . . . . 25
14 9 , 13 syl5bi 217
. . . . . . . . . . . . . . . . . . . . . . . 24
15 14 imp 429
. . . . . . . . . . . . . . . . . . . . . . 23
16 imassrn 5353
. . . . . . . . . . . . . . . . . . . . . . 23
17 15 , 16 jctil 537
. . . . . . . . . . . . . . . . . . . . . 22
18 sseq1 3524
. . . . . . . . . . . . . . . . . . . . . . . . 25
19 neeq1 2738
. . . . . . . . . . . . . . . . . . . . . . . . 25
20 18 , 19 anbi12d 710
. . . . . . . . . . . . . . . . . . . . . . . 24
21 raleq 3054
. . . . . . . . . . . . . . . . . . . . . . . . 25
22 21 rexeqbi1dv 3063
. . . . . . . . . . . . . . . . . . . . . . . 24
23 20 , 22 imbi12d 320
. . . . . . . . . . . . . . . . . . . . . . 23
24 23 spcgv 3194
. . . . . . . . . . . . . . . . . . . . . 22
25 17 , 24 syl7 68
. . . . . . . . . . . . . . . . . . . . 21
26 8 , 25 syl 16
. . . . . . . . . . . . . . . . . . . 20
27 6 , 26 syl5bi 217
. . . . . . . . . . . . . . . . . . 19
28 27 com23 78
. . . . . . . . . . . . . . . . . 18
29 28 expd 436
. . . . . . . . . . . . . . . . 17
30 29 anabsi5 817
. . . . . . . . . . . . . . . 16
31 30 impd 431
. . . . . . . . . . . . . . 15
32 fores 5809
. . . . . . . . . . . . . . . 16
33 fvres 5885
. . . . . . . . . . . . . . . . . . . . . 22
34 fvres 5885
. . . . . . . . . . . . . . . . . . . . . 22
35 33 , 34 breqan12rd 4468
. . . . . . . . . . . . . . . . . . . . 21
36 vex 3112
. . . . . . . . . . . . . . . . . . . . . 22
37 vex 3112
. . . . . . . . . . . . . . . . . . . . . 22
38 fveq2 5871
. . . . . . . . . . . . . . . . . . . . . . 23
39 38 breq1d 4462
. . . . . . . . . . . . . . . . . . . . . 22
40 fveq2 5871
. . . . . . . . . . . . . . . . . . . . . . 23
41 40 breq2d 4464
. . . . . . . . . . . . . . . . . . . . . 22
42 f1oweALT.1
. . . . . . . . . . . . . . . . . . . . . 22
43 36 , 37 , 39 , 41 , 42 brab 4775
. . . . . . . . . . . . . . . . . . . . 21
44 35 , 43 syl6rbbr 264
. . . . . . . . . . . . . . . . . . . 20
45 44 notbid 294
. . . . . . . . . . . . . . . . . . 19
46 45 ralbidva 2893
. . . . . . . . . . . . . . . . . 18
47 46 rexbiia 2958
. . . . . . . . . . . . . . . . 17
48 breq1 4455
. . . . . . . . . . . . . . . . . . . . 21
49 48 notbid 294
. . . . . . . . . . . . . . . . . . . 20
50 49 cbvfo 6192
. . . . . . . . . . . . . . . . . . 19
51 50 rexbidv 2968
. . . . . . . . . . . . . . . . . 18
52 breq2 4456
. . . . . . . . . . . . . . . . . . . . 21
53 52 notbid 294
. . . . . . . . . . . . . . . . . . . 20
54 53 ralbidv 2896
. . . . . . . . . . . . . . . . . . 19
55 54 cbvexfo 6193
. . . . . . . . . . . . . . . . . 18
56 51 , 55 bitrd 253
. . . . . . . . . . . . . . . . 17
57 47 , 56 syl5bb 257
. . . . . . . . . . . . . . . 16
58 32 , 57 syl 16
. . . . . . . . . . . . . . 15
59 31 , 58 sylibrd 234
. . . . . . . . . . . . . 14
60 59 exp4b 607
. . . . . . . . . . . . 13
61 60 com34 83
. . . . . . . . . . . 12
62 61 com23 78
. . . . . . . . . . 11
63 62 imp4a 589
. . . . . . . . . 10
64 63 alrimdv 1721
. . . . . . . . 9
65 df-fr 4843
. . . . . . . . 9
66 64 , 65 syl6ibr 227
. . . . . . . 8
67 freq2 4855
. . . . . . . . 9
68 67 biimpd 207
. . . . . . . 8
69 66 , 68 sylan9 657
. . . . . . 7
70 5 , 69 sylbi 195
. . . . . 6
71 4 , 70 sylan9r 658
. . . . 5
72 2 , 71 sylbi 195
. . . 4
73 1 , 72 syl 16
. . 3
74 df-f1o 5600
. . . . 5
75 fveq2 5871
. . . . . . . . . . 11
76 75 breq1d 4462
. . . . . . . . . 10
77 fveq2 5871
. . . . . . . . . . 11
78 77 breq2d 4464
. . . . . . . . . 10
79 37 , 36 , 76 , 78 , 42 brab 4775
. . . . . . . . 9
80 79 a1i 11
. . . . . . . 8
81 f1fveq 6170
. . . . . . . . 9
82 81 bicomd 201
. . . . . . . 8
83 43 a1i 11
. . . . . . . 8
84 80 , 82 , 83 3orbi123d 1298
. . . . . . 7
85 84 2ralbidva 2899
. . . . . 6
86 breq1 4455
. . . . . . . . . 10
87 eqeq1 2461
. . . . . . . . . 10
88 breq2 4456
. . . . . . . . . 10
89 86 , 87 , 88 3orbi123d 1298
. . . . . . . . 9
90 89 ralbidv 2896
. . . . . . . 8
91 90 cbvfo 6192
. . . . . . 7
92 breq2 4456
. . . . . . . . . 10
93 eqeq2 2472
. . . . . . . . . 10
94 breq1 4455
. . . . . . . . . 10
95 92 , 93 , 94 3orbi123d 1298
. . . . . . . . 9
96 95 cbvfo 6192
. . . . . . . 8
97 96 ralbidv 2896
. . . . . . 7
98 91 , 97 bitrd 253
. . . . . 6
99 85 , 98 sylan9bb 699
. . . . 5
100 74 , 99 sylbi 195
. . . 4
101 100 biimprd 223
. . 3
102 73 , 101 anim12d 563
. 2
103 dfwe2 6617
. 2
104 dfwe2 6617
. 2
105 102 , 103 ,
104 3imtr4g 270
1