Step Hyp Ref
Expression
1 nfv 1707
. . 3
2 flift.1
. . . . 5
3 nfmpt1 4541
. . . . . 6
4 3 nfrn 5250
. . . . 5
5 2 , 4 nfcxfr 2617
. . . 4
6 5 nffun 5615
. . 3
7 fveq2 5871
. . . . . . 7
8 simplr 755
. . . . . . . . 9
9 flift.2
. . . . . . . . . . 11
10 flift.3
. . . . . . . . . . 11
11 2 , 9 , 10 fliftel1 6208
. . . . . . . . . 10
12 11 ad2ant2r 746
. . . . . . . . 9
13 funbrfv 5911
. . . . . . . . 9
14 8 , 12 , 13 sylc 60
. . . . . . . 8
15 simprr 757
. . . . . . . . . . 11
16 eqidd 2458
. . . . . . . . . . 11
17 eqidd 2458
. . . . . . . . . . 11
18 fliftfun.4
. . . . . . . . . . . . . 14
19 18 eqeq2d 2471
. . . . . . . . . . . . 13
20 fliftfun.5
. . . . . . . . . . . . . 14
21 20 eqeq2d 2471
. . . . . . . . . . . . 13
22 19 , 21 anbi12d 710
. . . . . . . . . . . 12
23 22 rspcev 3210
. . . . . . . . . . 11
24 15 , 16 , 17 , 23 syl12anc 1226
. . . . . . . . . 10
25 2 , 9 , 10 fliftel 6207
. . . . . . . . . . 11
26 25 ad2antrr 725
. . . . . . . . . 10
27 24 , 26 mpbird 232
. . . . . . . . 9
28 funbrfv 5911
. . . . . . . . 9
29 8 , 27 , 28 sylc 60
. . . . . . . 8
30 14 , 29 eqeq12d 2479
. . . . . . 7
31 7 , 30 syl5ib 219
. . . . . 6
32 31 anassrs 648
. . . . 5
33 32 ralrimiva 2871
. . . 4
34 33 exp31 604
. . 3
35 1 , 6 , 34 ralrimd 2861
. 2
36 2 , 9 , 10 fliftel 6207
. . . . . . . . 9
37 2 , 9 , 10 fliftel 6207
. . . . . . . . . 10
38 18 eqeq2d 2471
. . . . . . . . . . . 12
39 20 eqeq2d 2471
. . . . . . . . . . . 12
40 38 , 39 anbi12d 710
. . . . . . . . . . 11
41 40 cbvrexv 3085
. . . . . . . . . 10
42 37 , 41 syl6bb 261
. . . . . . . . 9
43 36 , 42 anbi12d 710
. . . . . . . 8
44 43 biimpd 207
. . . . . . 7
45 reeanv 3025
. . . . . . . 8
46 r19.29 2992
. . . . . . . . . 10
47 r19.29 2992
. . . . . . . . . . . 12
48 eqtr2 2484
. . . . . . . . . . . . . . . . 17
49 48 ad2ant2r 746
. . . . . . . . . . . . . . . 16
50 49 imim1i 58
. . . . . . . . . . . . . . 15
51 50 imp 429
. . . . . . . . . . . . . 14
52 simprlr 764
. . . . . . . . . . . . . 14
53 simprrr 766
. . . . . . . . . . . . . 14
54 51 , 52 , 53 3eqtr4d 2508
. . . . . . . . . . . . 13
55 54 rexlimivw 2946
. . . . . . . . . . . 12
56 47 , 55 syl 16
. . . . . . . . . . 11
57 56 rexlimivw 2946
. . . . . . . . . 10
58 46 , 57 syl 16
. . . . . . . . 9
59 58 ex 434
. . . . . . . 8
60 45 , 59 syl5bir 218
. . . . . . 7
61 44 , 60 syl9 71
. . . . . 6
62 61 alrimdv 1721
. . . . 5
63 62 alrimdv 1721
. . . 4
64 63 alrimdv 1721
. . 3
65 2 , 9 , 10 fliftrel 6206
. . . . 5
66 relxp 5115
. . . . 5
67 relss 5095
. . . . 5
68 65 , 66 , 67 mpisyl 18
. . . 4
69 dffun2 5603
. . . . 5
70 69 baib 903
. . . 4
71 68 , 70 syl 16
. . 3
72 64 , 71 sylibrd 234
. 2
73 35 , 72 impbid 191
1