Step | Hyp | Ref
| Expression |
1 | | isf32lem.c |
. . . . 5
|
2 | 1 | adantr 465 |
. . . 4
|
3 | | isf32lem.a |
. . . . . . . . . 10
|
4 | | ffn 5736 |
. . . . . . . . . 10
|
5 | 3, 4 | syl 16 |
. . . . . . . . 9
|
6 | | peano2 6720 |
. . . . . . . . 9
|
7 | | fnfvelrn 6028 |
. . . . . . . . 9
|
8 | 5, 6, 7 | syl2an 477 |
. . . . . . . 8
|
9 | 8 | adantr 465 |
. . . . . . 7
|
10 | | intss1 4301 |
. . . . . . 7
|
11 | 9, 10 | syl 16 |
. . . . . 6
|
12 | | fvelrnb 5920 |
. . . . . . . . . . 11
|
13 | 5, 12 | syl 16 |
. . . . . . . . . 10
|
14 | 13 | ad2antrr 725 |
. . . . . . . . 9
|
15 | | simplrr 762 |
. . . . . . . . . . . . . . 15
|
16 | 6 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
|
17 | | simpr 461 |
. . . . . . . . . . . . . . 15
|
18 | | simplrl 761 |
. . . . . . . . . . . . . . 15
|
19 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . 18
|
21 | 20 | imbi2d 316 |
. . . . . . . . . . . . . . . . 17
|
22 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 22 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . 18
|
24 | 23 | imbi2d 316 |
. . . . . . . . . . . . . . . . 17
|
25 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 25 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | imbi2d 316 |
. . . . . . . . . . . . . . . . 17
|
28 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 28 | eqeq2d 2471 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | imbi2d 316 |
. . . . . . . . . . . . . . . . 17
|
31 | | eqid 2457 |
. . . . . . . . . . . . . . . . . 18
|
32 | 31 | a1ii 27 |
. . . . . . . . . . . . . . . . 17
|
33 | | elex 3118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
34 | | sucexb 6644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | 33, 34 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
36 | 35 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | | sucssel 4975 |
. . . . . . . . . . . . . . . . . . . . . 22
|
38 | 36, 37 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
|
39 | 38 | imp 429 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | | eleq2 2530 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
41 | | suceq 4948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
42 | 41 | fveq2d 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
43 | | fveq2 5871 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
44 | 42, 43 | eqeq12d 2479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
45 | 40, 44 | imbi12d 320 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | rspcv 3206 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | com23 78 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 39, 48 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | eqtr3 2485 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 50 | expcom 435 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 49, 51 | syl6 33 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | a2d 26 |
. . . . . . . . . . . . . . . . 17
|
54 | 21, 24, 27, 30, 32, 53 | findsg 6727 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | impr 619 |
. . . . . . . . . . . . . . 15
|
56 | 15, 16, 17, 18, 55 | syl22anc 1229 |
. . . . . . . . . . . . . 14
|
57 | | eqimss 3555 |
. . . . . . . . . . . . . 14
|
58 | 56, 57 | syl 16 |
. . . . . . . . . . . . 13
|
59 | 6 | ad3antlr 730 |
. . . . . . . . . . . . . 14
|
60 | | simplrr 762 |
. . . . . . . . . . . . . 14
|
61 | | simpr 461 |
. . . . . . . . . . . . . 14
|
62 | | simplll 759 |
. . . . . . . . . . . . . 14
|
63 | | isf32lem.b |
. . . . . . . . . . . . . . 15
|
64 | 3, 63, 1 | isf32lem1 8754 |
. . . . . . . . . . . . . 14
|
65 | 59, 60, 61, 62, 64 | syl22anc 1229 |
. . . . . . . . . . . . 13
|
66 | | nnord 6708 |
. . . . . . . . . . . . . . . 16
|
67 | 6, 66 | syl 16 |
. . . . . . . . . . . . . . 15
|
68 | 67 | ad2antlr 726 |
. . . . . . . . . . . . . 14
|
69 | | nnord 6708 |
. . . . . . . . . . . . . . 15
|
70 | 69 | ad2antll 728 |
. . . . . . . . . . . . . 14
|
71 | | ordtri2or2 4979 |
. . . . . . . . . . . . . 14
|
72 | 68, 70, 71 | syl2anc 661 |
. . . . . . . . . . . . 13
|
73 | 58, 65, 72 | mpjaodan 786 |
. . . . . . . . . . . 12
|
74 | 73 | anassrs 648 |
. . . . . . . . . . 11
|
75 | | sseq2 3525 |
. . . . . . . . . . 11
|
76 | 74, 75 | syl5ibcom 220 |
. . . . . . . . . 10
|
77 | 76 | rexlimdva 2949 |
. . . . . . . . 9
|
78 | 14, 77 | sylbid 215 |
. . . . . . . 8
|
79 | 78 | ralrimiv 2869 |
. . . . . . 7
|
80 | | ssint 4302 |
. . . . . . 7
|
81 | 79, 80 | sylibr 212 |
. . . . . 6
|
82 | 11, 81 | eqssd 3520 |
. . . . 5
|
83 | 82, 9 | eqeltrd 2545 |
. . . 4
|
84 | 2, 83 | mtand 659 |
. . 3
|
85 | | rexnal 2905 |
. . 3
|
86 | 84, 85 | sylibr 212 |
. 2
|
87 | | suceq 4948 |
. . . . . . . 8
|
88 | 87 | fveq2d 5875 |
. . . . . . 7
|
89 | | fveq2 5871 |
. . . . . . 7
|
90 | 88, 89 | sseq12d 3532 |
. . . . . 6
|
91 | 90 | cbvralv 3084 |
. . . . 5
|
92 | 63, 91 | sylib 196 |
. . . 4
|
93 | 92 | adantr 465 |
. . 3
|
94 | | pm4.61 426 |
. . . . 5
|
95 | | dfpss2 3588 |
. . . . . . 7
|
96 | 95 | simplbi2 625 |
. . . . . 6
|
97 | 96 | anim2d 565 |
. . . . 5
|
98 | 94, 97 | syl5bi 217 |
. . . 4
|
99 | 98 | ralimi 2850 |
. . 3
|
100 | | rexim 2922 |
. . 3
|
101 | 93, 99, 100 | 3syl 20 |
. 2
|
102 | 86, 101 | mpd 15 |
1
|