Step | Hyp | Ref
| Expression |
1 | | isf32lem.c |
. . . . 5
|
2 | 1 | adantr 481 |
. . . 4
|
3 | | isf32lem.a |
. . . . . . . . . 10
|
4 | | ffn 6045 |
. . . . . . . . . 10
|
5 | 3, 4 | syl 17 |
. . . . . . . . 9
|
6 | | peano2 7086 |
. . . . . . . . 9
|
7 | | fnfvelrn 6356 |
. . . . . . . . 9
|
8 | 5, 6, 7 | syl2an 494 |
. . . . . . . 8
|
9 | 8 | adantr 481 |
. . . . . . 7
|
10 | | intss1 4492 |
. . . . . . 7
|
11 | 9, 10 | syl 17 |
. . . . . 6
|
12 | | fvelrnb 6243 |
. . . . . . . . . . 11
|
13 | 5, 12 | syl 17 |
. . . . . . . . . 10
|
14 | 13 | ad2antrr 762 |
. . . . . . . . 9
|
15 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
16 | 6 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
|
17 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
18 | | simplrl 800 |
. . . . . . . . . . . . . . 15
|
19 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
21 | 20 | imbi2d 330 |
. . . . . . . . . . . . . . . . 17
|
22 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 22 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
24 | 23 | imbi2d 330 |
. . . . . . . . . . . . . . . . 17
|
25 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 25 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | imbi2d 330 |
. . . . . . . . . . . . . . . . 17
|
28 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 28 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | imbi2d 330 |
. . . . . . . . . . . . . . . . 17
|
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
32 | 31 | 2a1i 12 |
. . . . . . . . . . . . . . . . 17
|
33 | | elex 3212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
34 | | sucexb 7009 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | 33, 34 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | | sucssel 5819 |
. . . . . . . . . . . . . . . . . . . . . 22
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
39 | 38 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
41 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
42 | 41 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
43 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
44 | 42, 43 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
45 | 40, 44 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
46 | 45 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | 46 | com23 86 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 39, 48 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | eqtr3 2643 |
. . . . . . . . . . . . . . . . . . . 20
|
51 | 50 | expcom 451 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 49, 51 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | a2d 29 |
. . . . . . . . . . . . . . . . 17
|
54 | 21, 24, 27, 30, 32, 53 | findsg 7093 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | impr 649 |
. . . . . . . . . . . . . . 15
|
56 | 15, 16, 17, 18, 55 | syl22anc 1327 |
. . . . . . . . . . . . . 14
|
57 | | eqimss 3657 |
. . . . . . . . . . . . . 14
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
|
59 | 6 | ad3antlr 767 |
. . . . . . . . . . . . . 14
|
60 | | simplrr 801 |
. . . . . . . . . . . . . 14
|
61 | | simpr 477 |
. . . . . . . . . . . . . 14
|
62 | | simplll 798 |
. . . . . . . . . . . . . 14
|
63 | | isf32lem.b |
. . . . . . . . . . . . . . 15
|
64 | 3, 63, 1 | isf32lem1 9175 |
. . . . . . . . . . . . . 14
|
65 | 59, 60, 61, 62, 64 | syl22anc 1327 |
. . . . . . . . . . . . 13
|
66 | | nnord 7073 |
. . . . . . . . . . . . . . . 16
|
67 | 6, 66 | syl 17 |
. . . . . . . . . . . . . . 15
|
68 | 67 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
69 | | nnord 7073 |
. . . . . . . . . . . . . . 15
|
70 | 69 | ad2antll 765 |
. . . . . . . . . . . . . 14
|
71 | | ordtri2or2 5823 |
. . . . . . . . . . . . . 14
|
72 | 68, 70, 71 | syl2anc 693 |
. . . . . . . . . . . . 13
|
73 | 58, 65, 72 | mpjaodan 827 |
. . . . . . . . . . . 12
|
74 | 73 | anassrs 680 |
. . . . . . . . . . 11
|
75 | | sseq2 3627 |
. . . . . . . . . . 11
|
76 | 74, 75 | syl5ibcom 235 |
. . . . . . . . . 10
|
77 | 76 | rexlimdva 3031 |
. . . . . . . . 9
|
78 | 14, 77 | sylbid 230 |
. . . . . . . 8
|
79 | 78 | ralrimiv 2965 |
. . . . . . 7
|
80 | | ssint 4493 |
. . . . . . 7
|
81 | 79, 80 | sylibr 224 |
. . . . . 6
|
82 | 11, 81 | eqssd 3620 |
. . . . 5
|
83 | 82, 9 | eqeltrd 2701 |
. . . 4
|
84 | 2, 83 | mtand 691 |
. . 3
|
85 | | rexnal 2995 |
. . 3
|
86 | 84, 85 | sylibr 224 |
. 2
|
87 | | suceq 5790 |
. . . . . . . 8
|
88 | 87 | fveq2d 6195 |
. . . . . . 7
|
89 | | fveq2 6191 |
. . . . . . 7
|
90 | 88, 89 | sseq12d 3634 |
. . . . . 6
|
91 | 90 | cbvralv 3171 |
. . . . 5
|
92 | 63, 91 | sylib 208 |
. . . 4
|
93 | 92 | adantr 481 |
. . 3
|
94 | | pm4.61 442 |
. . . . 5
|
95 | | dfpss2 3692 |
. . . . . . 7
|
96 | 95 | simplbi2 655 |
. . . . . 6
|
97 | 96 | anim2d 589 |
. . . . 5
|
98 | 94, 97 | syl5bi 232 |
. . . 4
|
99 | 98 | ralimi 2952 |
. . 3
|
100 | | rexim 3008 |
. . 3
|
101 | 93, 99, 100 | 3syl 18 |
. 2
|
102 | 86, 101 | mpd 15 |
1
|