Step Hyp Ref
Expression 1 ssid 3522 . 2
2 tfrlem1.1 . . 3
3 sseq1 3524 . . . . . 6
4 raleq 3054 . . . . . 6
5 3 , 4 imbi12d 320 . . . . 5
6 5 imbi2d 316 . . . 4
7 sseq1 3524 . . . . . 6
8 raleq 3054 . . . . . 6
9 7 , 8 imbi12d 320 . . . . 5
10 9 imbi2d 316 . . . 4
11 r19.21v 2862 . . . . 5
12 tfrlem1.2 . . . . . . . . . . . . . . . . 17
13 12 ad4antr 731 . . . . . . . . . . . . . . . 16
14 13 simpld 459 . . . . . . . . . . . . . . 15
15 funfn 5622 . . . . . . . . . . . . . . 15
16 14 , 15 sylib 196 . . . . . . . . . . . . . 14
17 eloni 4893 . . . . . . . . . . . . . . . . . 18
18 17 ad3antlr 730 . . . . . . . . . . . . . . . . 17
19 ordelss 4899 . . . . . . . . . . . . . . . . 17
20 18 , 19 sylan 471 . . . . . . . . . . . . . . . 16
21 simplr 755 . . . . . . . . . . . . . . . 16
22 20 , 21 sstrd 3513 . . . . . . . . . . . . . . 15
23 13 simprd 463 . . . . . . . . . . . . . . 15
24 22 , 23 sstrd 3513 . . . . . . . . . . . . . 14
25 fnssres 5699 . . . . . . . . . . . . . 14
26 16 , 24 , 25 syl2anc 661 . . . . . . . . . . . . 13
27 tfrlem1.3 . . . . . . . . . . . . . . . . 17
28 27 ad4antr 731 . . . . . . . . . . . . . . . 16
29 28 simpld 459 . . . . . . . . . . . . . . 15
30 funfn 5622 . . . . . . . . . . . . . . 15
31 29 , 30 sylib 196 . . . . . . . . . . . . . 14
32 28 simprd 463 . . . . . . . . . . . . . . 15
33 22 , 32 sstrd 3513 . . . . . . . . . . . . . 14
34 fnssres 5699 . . . . . . . . . . . . . 14
35 31 , 33 , 34 syl2anc 661 . . . . . . . . . . . . 13
36 simpr 461 . . . . . . . . . . . . . . 15
37 simplr 755 . . . . . . . . . . . . . . . 16
38 simp-4r 768 . . . . . . . . . . . . . . . 16
39 22 adantr 465 . . . . . . . . . . . . . . . 16
40 sseq1 3524 . . . . . . . . . . . . . . . . . 18
41 raleq 3054 . . . . . . . . . . . . . . . . . 18
42 40 , 41 imbi12d 320 . . . . . . . . . . . . . . . . 17
43 42 rspcv 3206 . . . . . . . . . . . . . . . 16
44 37 , 38 , 39 , 43 syl3c 61 . . . . . . . . . . . . . . 15
45 fveq2 5871 . . . . . . . . . . . . . . . . 17
46 fveq2 5871 . . . . . . . . . . . . . . . . 17
47 45 , 46 eqeq12d 2479 . . . . . . . . . . . . . . . 16
48 47 rspcv 3206 . . . . . . . . . . . . . . 15
49 36 , 44 , 48 sylc 60 . . . . . . . . . . . . . 14
50 fvres 5885 . . . . . . . . . . . . . . 15
51 50 adantl 466 . . . . . . . . . . . . . 14
52 fvres 5885 . . . . . . . . . . . . . . 15
53 52 adantl 466 . . . . . . . . . . . . . 14
54 49 , 51 , 53 3eqtr4d 2508 . . . . . . . . . . . . 13
55 26 , 35 , 54 eqfnfvd 5984 . . . . . . . . . . . 12
56 55 fveq2d 5875 . . . . . . . . . . 11
57 simpr 461 . . . . . . . . . . . . 13
58 57 sselda 3503 . . . . . . . . . . . 12
59 tfrlem1.4 . . . . . . . . . . . . 13
60 59 ad4antr 731 . . . . . . . . . . . 12
61 fveq2 5871 . . . . . . . . . . . . . 14
62 reseq2 5273 . . . . . . . . . . . . . . 15
63 62 fveq2d 5875 . . . . . . . . . . . . . 14
64 61 , 63 eqeq12d 2479 . . . . . . . . . . . . 13
65 64 rspcva 3208 . . . . . . . . . . . 12
66 58 , 60 , 65 syl2anc 661 . . . . . . . . . . 11
67 tfrlem1.5 . . . . . . . . . . . . 13
68 67 ad4antr 731 . . . . . . . . . . . 12
69 fveq2 5871 . . . . . . . . . . . . . 14
70 reseq2 5273 . . . . . . . . . . . . . . 15
71 70 fveq2d 5875 . . . . . . . . . . . . . 14
72 69 , 71 eqeq12d 2479 . . . . . . . . . . . . 13
73 72 rspcva 3208 . . . . . . . . . . . 12
74 58 , 68 , 73 syl2anc 661 . . . . . . . . . . 11
75 56 , 66 , 74 3eqtr4d 2508 . . . . . . . . . 10
76 75 ralrimiva 2871 . . . . . . . . 9
77 61 , 69 eqeq12d 2479 . . . . . . . . . 10
78 77 cbvralv 3084 . . . . . . . . 9
79 76 , 78 sylibr 212 . . . . . . . 8
80 79 exp31 604 . . . . . . 7
81 80 expcom 435 . . . . . 6
82 81 a2d 26 . . . . 5
83 11 , 82 syl5bi 217 . . . 4
84 6 , 10 , 83 tfis3 6692 . . 3
85 2 , 84 mpcom 36 . 2
86 1 , 85 mpi 17 1
