Step Hyp Ref
Expression 1 resixp 7524 . . . 4
2 resixpfo.1 . . . 4
3 1 , 2 fmptd 6055 . . 3
4 3 adantr 465 . 2
5 n0 3794 . . . 4
6 eleq1 2529 . . . . . . . . . . . 12
7 6 ifbid 3963 . . . . . . . . . . 11
8 id 22 . . . . . . . . . . 11
9 7 , 8 fveq12d 5877 . . . . . . . . . 10
10 9 cbvmptv 4543 . . . . . . . . 9
11 vex 3112 . . . . . . . . . . . . 13
12 11 elixp 7496 . . . . . . . . . . . 12
13 12 simprbi 464 . . . . . . . . . . 11
14 vex 3112 . . . . . . . . . . . . . . . . 17
15 14 elixp 7496 . . . . . . . . . . . . . . . 16
16 15 simprbi 464 . . . . . . . . . . . . . . 15
17 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
18 17 eleq1d 2526 . . . . . . . . . . . . . . . . . 18
19 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
20 19 eleq1d 2526 . . . . . . . . . . . . . . . . . 18
21 simpl 457 . . . . . . . . . . . . . . . . . . 19
22 21 imp 429 . . . . . . . . . . . . . . . . . 18
23 simplrr 762 . . . . . . . . . . . . . . . . . 18
24 18 , 20 , 22 , 23 ifbothda 3976 . . . . . . . . . . . . . . . . 17
25 24 exp32 605 . . . . . . . . . . . . . . . 16
26 25 ralimi2 2847 . . . . . . . . . . . . . . 15
27 16 , 26 syl 16 . . . . . . . . . . . . . 14
28 27 adantl 466 . . . . . . . . . . . . 13
29 ralim 2846 . . . . . . . . . . . . 13
30 28 , 29 syl 16 . . . . . . . . . . . 12
31 30 imp 429 . . . . . . . . . . 11
32 13 , 31 sylan2 474 . . . . . . . . . 10
33 n0i 3789 . . . . . . . . . . . . 13
34 ixpprc 7510 . . . . . . . . . . . . 13
35 33 , 34 nsyl2 127 . . . . . . . . . . . 12
36 35 adantl 466 . . . . . . . . . . 11
37 mptelixpg 7526 . . . . . . . . . . 11
38 36 , 37 syl 16 . . . . . . . . . 10
39 32 , 38 mpbird 232 . . . . . . . . 9
40 10 , 39 syl5eqel 2549 . . . . . . . 8
41 iftrue 3947 . . . . . . . . . . . . . 14
42 41 fveq1d 5873 . . . . . . . . . . . . 13
43 42 mpteq2ia 4534 . . . . . . . . . . . 12
44 resmpt 5328 . . . . . . . . . . . . 13
45 44 ad2antrr 725 . . . . . . . . . . . 12
46 ixpfn 7495 . . . . . . . . . . . . . 14
47 46 ad2antlr 726 . . . . . . . . . . . . 13
48 dffn5 5918 . . . . . . . . . . . . 13
49 47 , 48 sylib 196 . . . . . . . . . . . 12
50 43 , 45 , 49 3eqtr4a 2524 . . . . . . . . . . 11
51 50 , 14 syl6eqel 2553 . . . . . . . . . 10
52 reseq1 5272 . . . . . . . . . . 11
53 52 , 2 fvmptg 5954 . . . . . . . . . 10
54 40 , 51 , 53 syl2anc 661 . . . . . . . . 9
55 54 , 50 eqtr2d 2499 . . . . . . . 8
56 fveq2 5871 . . . . . . . . . 10
57 56 eqeq2d 2471 . . . . . . . . 9
58 57 rspcev 3210 . . . . . . . 8
59 40 , 55 , 58 syl2anc 661 . . . . . . 7
60 59 ex 434 . . . . . 6
61 60 ralrimdva 2875 . . . . 5
62 61 exlimdv 1724 . . . 4
63 5 , 62 syl5bi 217 . . 3
64 63 imp 429 . 2
65 dffo3 6046 . 2
66 4 , 64 , 65 sylanbrc 664 1
