Step Hyp Ref
Expression 1 isf32lem.g . . . 4
2 ssab2 3583 . . . . . . 7
3 iotacl 5579 . . . . . . 7
4 2 , 3 sseldi 3501 . . . . . 6
5 iotanul 5571 . . . . . . 7
6 peano1 6719 . . . . . . 7
7 5 , 6 syl6eqel 2553 . . . . . 6
8 4 , 7 pm2.61i 164 . . . . 5
9 8 a1i 11 . . . 4
10 1 , 9 fmpti 6054 . . 3
11 10 a1i 11 . 2
12 isf32lem.a . . . . . 6
13 isf32lem.b . . . . . 6
14 isf32lem.c . . . . . 6
15 isf32lem.d . . . . . 6
16 isf32lem.e . . . . . 6
17 isf32lem.f . . . . . 6
18 12 , 13 , 14 , 15 , 16 , 17 isf32lem6 8759 . . . . 5
19 n0 3794 . . . . 5
20 18 , 19 sylib 196 . . . 4
21 12 , 13 , 14 , 15 , 16 , 17 isf32lem8 8761 . . . . . . . . 9
22 21 sselda 3503 . . . . . . . 8
23 eleq1 2529 . . . . . . . . . . . . 13
24 23 anbi2d 703 . . . . . . . . . . . 12
25 24 iotabidv 5577 . . . . . . . . . . 11
26 iotaex 5573 . . . . . . . . . . 11
27 25 , 1 , 26 fvmpt3i 5960 . . . . . . . . . 10
28 22 , 27 syl 16 . . . . . . . . 9
29 simp1r 1021 . . . . . . . . . . . . . . . 16
30 simpl1 999 . . . . . . . . . . . . . . . . . . . . . 22
31 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23
32 31 necomd 2728 . . . . . . . . . . . . . . . . . . . . . 22
33 simpl2 1000 . . . . . . . . . . . . . . . . . . . . . 22
34 simpl3 1001 . . . . . . . . . . . . . . . . . . . . . 22
35 12 , 13 , 14 , 15 , 16 , 17 isf32lem7 8760 . . . . . . . . . . . . . . . . . . . . . 22
36 30 , 32 , 33 , 34 , 35 syl22anc 1229 . . . . . . . . . . . . . . . . . . . . 21
37 disj1 3869 . . . . . . . . . . . . . . . . . . . . 21
38 36 , 37 sylib 196 . . . . . . . . . . . . . . . . . . . 20
39 38 ex 434 . . . . . . . . . . . . . . . . . . 19
40 sp 1859 . . . . . . . . . . . . . . . . . . 19
41 39 , 40 syl6 33 . . . . . . . . . . . . . . . . . 18
42 41 com23 78 . . . . . . . . . . . . . . . . 17
43 42 3adant1r 1221 . . . . . . . . . . . . . . . 16
44 29 , 43 mpd 15 . . . . . . . . . . . . . . 15
45 44 necon4ad 2677 . . . . . . . . . . . . . 14
46 45 3expia 1198 . . . . . . . . . . . . 13
47 46 impd 431 . . . . . . . . . . . 12
48 eleq1 2529 . . . . . . . . . . . . . . . 16
49 fveq2 5871 . . . . . . . . . . . . . . . . 17
50 49 eleq2d 2527 . . . . . . . . . . . . . . . 16
51 48 , 50 anbi12d 710 . . . . . . . . . . . . . . 15
52 51 biimprcd 225 . . . . . . . . . . . . . 14
53 52 ancoms 453 . . . . . . . . . . . . 13
54 53 adantll 713 . . . . . . . . . . . 12
55 47 , 54 impbid 191 . . . . . . . . . . 11
56 55 iota5 5576 . . . . . . . . . 10
57 56 an32s 804 . . . . . . . . 9
58 28 , 57 eqtr2d 2499 . . . . . . . 8
59 22 , 58 jca 532 . . . . . . 7
60 59 ex 434 . . . . . 6
61 60 eximdv 1710 . . . . 5
62 df-rex 2813 . . . . 5
63 61 , 62 syl6ibr 227 . . . 4
64 20 , 63 mpd 15 . . 3
65 64 ralrimiva 2871 . 2
66 dffo3 6046 . 2
67 11 , 65 , 66 sylanbrc 664 1
