Step Hyp Ref
Expression 1 fdm 5740 . . . . . . . 8
2 vex 3112 . . . . . . . . 9
3 2 dmex 6733 . . . . . . . 8
4 1 , 3 syl6eqelr 2554 . . . . . . 7
5 coftr.1 . . . . . . . . 9
6 fveq2 5871 . . . . . . . . . . . . 13
7 6 sseq1d 3530 . . . . . . . . . . . 12
8 7 rabbidv 3101 . . . . . . . . . . 11
9 8 inteqd 4291 . . . . . . . . . 10
10 9 cbvmptv 4543 . . . . . . . . 9
11 5 , 10 eqtri 2486 . . . . . . . 8
12 mptexg 6142 . . . . . . . 8
13 11 , 12 syl5eqel 2549 . . . . . . 7
14 4 , 13 syl 16 . . . . . 6
15 14 ad2antrl 727 . . . . 5
16 ffn 5736 . . . . . . . . 9
17 smodm2 7045 . . . . . . . . 9
18 16 , 17 sylan 471 . . . . . . . 8
19 18 3adant3 1016 . . . . . . 7
20 19 adantr 465 . . . . . 6
21 simpl3 1001 . . . . . 6
22 simprl 756 . . . . . 6
23 simpl1 999 . . . . . . . 8
24 simpl2 1000 . . . . . . . . 9
25 ffvelrn 6029 . . . . . . . . . 10
26 25 3ad2antl3 1160 . . . . . . . . 9
27 sseq1 3524 . . . . . . . . . . 11
28 27 rexbidv 2968 . . . . . . . . . 10
29 28 rspccv 3207 . . . . . . . . 9
30 24 , 26 , 29 sylc 60 . . . . . . . 8
31 ssrab2 3584 . . . . . . . . . . . . 13
32 ordsson 6625 . . . . . . . . . . . . 13
33 31 , 32 syl5ss 3514 . . . . . . . . . . . 12
34 fveq2 5871 . . . . . . . . . . . . . . 15
35 34 sseq2d 3531 . . . . . . . . . . . . . 14
36 35 rspcev 3210 . . . . . . . . . . . . 13
37 rabn0 3805 . . . . . . . . . . . . 13
38 36 , 37 sylibr 212 . . . . . . . . . . . 12
39 oninton 6635 . . . . . . . . . . . 12
40 33 , 38 , 39 syl2an 477 . . . . . . . . . . 11
41 eloni 4893 . . . . . . . . . . 11
42 40 , 41 syl 16 . . . . . . . . . 10
43 simpl 457 . . . . . . . . . 10
44 35 intminss 4313 . . . . . . . . . . 11
45 44 adantl 466 . . . . . . . . . 10
46 simprl 756 . . . . . . . . . 10
47 ordtr2 4927 . . . . . . . . . . 11
48 47 imp 429 . . . . . . . . . 10
49 42 , 43 , 45 , 46 , 48 syl22anc 1229 . . . . . . . . 9
50 49 rexlimdvaa 2950 . . . . . . . 8
51 23 , 30 , 50 sylc 60 . . . . . . 7
52 51 , 11 fmptd 6055 . . . . . 6
53 20 , 21 , 22 , 52 syl3anc 1228 . . . . 5
54 simprr 757 . . . . . . . 8
55 simpl1 999 . . . . . . . 8
56 ffvelrn 6029 . . . . . . . . . 10
57 sseq1 3524 . . . . . . . . . . . 12
58 57 rexbidv 2968 . . . . . . . . . . 11
59 58 rspccv 3207 . . . . . . . . . 10
60 56 , 59 syl5 32 . . . . . . . . 9
61 60 expdimp 437 . . . . . . . 8
62 54 , 55 , 61 syl2anc 661 . . . . . . 7
63 55 , 16 syl 16 . . . . . . . 8
64 simpl2 1000 . . . . . . . 8
65 simpr 461 . . . . . . . . . . . . . . . 16
66 65 , 51 jca 532 . . . . . . . . . . . . . . 15
67 35 elrab 3257 . . . . . . . . . . . . . . . . . . 19
68 sstr2 3510 . . . . . . . . . . . . . . . . . . . . . . 23
69 smoword 7056 . . . . . . . . . . . . . . . . . . . . . . . 24
70 69 biimprd 223 . . . . . . . . . . . . . . . . . . . . . . 23
71 68 , 70 syl9r 72 . . . . . . . . . . . . . . . . . . . . . 22
72 71 expr 615 . . . . . . . . . . . . . . . . . . . . 21
73 72 com23 78 . . . . . . . . . . . . . . . . . . . 20
74 73 imp4b 590 . . . . . . . . . . . . . . . . . . 19
75 67 , 74 syl5bi 217 . . . . . . . . . . . . . . . . . 18
76 75 ralrimiv 2869 . . . . . . . . . . . . . . . . 17
77 ssint 4302 . . . . . . . . . . . . . . . . 17
78 76 , 77 sylibr 212 . . . . . . . . . . . . . . . 16
79 9 , 5 fvmptg 5954 . . . . . . . . . . . . . . . . 17
80 79 sseq2d 3531 . . . . . . . . . . . . . . . 16
81 78 , 80 syl5ibrcom 222 . . . . . . . . . . . . . . 15
82 66 , 81 syl5 32 . . . . . . . . . . . . . 14
83 82 ex 434 . . . . . . . . . . . . 13
84 83 com23 78 . . . . . . . . . . . 12
85 84 expdimp 437 . . . . . . . . . . 11
86 85 reximdvai 2929 . . . . . . . . . 10
87 86 ancoms 453 . . . . . . . . 9
88 87 expr 615 . . . . . . . 8
89 20 , 21 , 22 , 63 , 64 , 88 syl32anc 1236 . . . . . . 7
90 62 , 89 mpdd 40 . . . . . 6
91 90 ralrimiv 2869 . . . . 5
92 feq1 5718 . . . . . . . 8
93 fveq1 5870 . . . . . . . . . . 11
94 93 sseq2d 3531 . . . . . . . . . 10
95 94 rexbidv 2968 . . . . . . . . 9
96 95 ralbidv 2896 . . . . . . . 8
97 92 , 96 anbi12d 710 . . . . . . 7
98 97 spcegv 3195 . . . . . 6
99 98 3impib 1194 . . . . 5
100 15 , 53 , 91 , 99 syl3anc 1228 . . . 4
101 100 ex 434 . . 3
102 101 exlimdv 1724 . 2
103 102 exlimiv 1722 1
