Step Hyp Ref
Expression 1 cff1 8659 . . 3
2 f1f 5786 . . . . . 6
3 fco 5746 . . . . . . . . . . . . . 14
4 3 adantlr 714 . . . . . . . . . . . . 13
5 4 adantr 465 . . . . . . . . . . . 12
6 r19.29 2992 . . . . . . . . . . . . . . . 16
7 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
8 ffn 5736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
9 smoword 7056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
10 9 biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
11 10 exp32 605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
12 8 , 11 sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
13 7 , 12 syl7 68 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
14 13 com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
15 14 expdimp 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
16 15 3imp2 1211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
17 sstr2 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
18 16 , 17 syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
19 fvco3 5950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
20 19 sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
21 20 adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
22 21 3ad2antr1 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
23 18 , 22 sylibrd 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
24 23 expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
25 24 3expia 1198 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
26 25 com4t 85 . . . . . . . . . . . . . . . . . . . . . . . . . 26
27 26 imp 429 . . . . . . . . . . . . . . . . . . . . . . . . 25
28 27 expcomd 438 . . . . . . . . . . . . . . . . . . . . . . . 24
29 28 imp31 432 . . . . . . . . . . . . . . . . . . . . . . 23
30 29 reximdva 2932 . . . . . . . . . . . . . . . . . . . . . 22
31 30 exp31 604 . . . . . . . . . . . . . . . . . . . . 21
32 31 com34 83 . . . . . . . . . . . . . . . . . . . 20
33 32 com23 78 . . . . . . . . . . . . . . . . . . 19
34 33 impd 431 . . . . . . . . . . . . . . . . . 18
35 34 com23 78 . . . . . . . . . . . . . . . . 17
36 35 rexlimdv 2947 . . . . . . . . . . . . . . . 16
37 6 , 36 syl5 32 . . . . . . . . . . . . . . 15
38 37 expdimp 437 . . . . . . . . . . . . . 14
39 38 ralimdv 2867 . . . . . . . . . . . . 13
40 39 impr 619 . . . . . . . . . . . 12
41 vex 3112 . . . . . . . . . . . . . 14
42 vex 3112 . . . . . . . . . . . . . 14
43 41 , 42 coex 6752 . . . . . . . . . . . . 13
44 feq1 5718 . . . . . . . . . . . . . 14
45 fveq1 5870 . . . . . . . . . . . . . . . . 17
46 45 sseq2d 3531 . . . . . . . . . . . . . . . 16
47 46 rexbidv 2968 . . . . . . . . . . . . . . 15
48 47 ralbidv 2896 . . . . . . . . . . . . . 14
49 44 , 48 anbi12d 710 . . . . . . . . . . . . 13
50 43 , 49 spcev 3201 . . . . . . . . . . . 12
51 5 , 40 , 50 syl2anc 661 . . . . . . . . . . 11
52 51 exp43 612 . . . . . . . . . 10
53 52 com24 87 . . . . . . . . 9
54 53 3impia 1193 . . . . . . . 8
55 54 exlimiv 1722 . . . . . . 7
56 55 com13 80 . . . . . 6
57 2 , 56 syl 16 . . . . 5
58 57 imp 429 . . . 4
59 58 exlimiv 1722 . . 3
60 1 , 59 syl 16 . 2
61 cfon 8656 . . 3
62 cfflb 8660 . . 3
63 61 , 62 mpan2 671 . 2
64 60 , 63 sylan9r 658 1
