Step | Hyp | Ref
| Expression |
1 | | frfnom 7530 |
. . . . . . 7
|
2 | | seqomlem.a |
. . . . . . . . 9
|
3 | 2 | reseq1i 5392 |
. . . . . . . 8
|
4 | 3 | fneq1i 5985 |
. . . . . . 7
|
5 | 1, 4 | mpbir 221 |
. . . . . 6
|
6 | | fvres 6207 |
. . . . . . . . 9
|
7 | 2 | seqomlem1 7545 |
. . . . . . . . 9
|
8 | 6, 7 | eqtrd 2656 |
. . . . . . . 8
|
9 | | fvex 6201 |
. . . . . . . . 9
|
10 | | opelxpi 5148 |
. . . . . . . . 9
|
11 | 9, 10 | mpan2 707 |
. . . . . . . 8
|
12 | 8, 11 | eqeltrd 2701 |
. . . . . . 7
|
13 | 12 | rgen 2922 |
. . . . . 6
|
14 | | ffnfv 6388 |
. . . . . 6
|
15 | 5, 13, 14 | mpbir2an 955 |
. . . . 5
|
16 | | frn 6053 |
. . . . 5
|
17 | 15, 16 | ax-mp 5 |
. . . 4
|
18 | | df-br 4654 |
. . . . . . . . . 10
|
19 | | fvelrnb 6243 |
. . . . . . . . . . 11
|
20 | 5, 19 | ax-mp 5 |
. . . . . . . . . 10
|
21 | | fvres 6207 |
. . . . . . . . . . . 12
|
22 | 21 | eqeq1d 2624 |
. . . . . . . . . . 11
|
23 | 22 | rexbiia 3040 |
. . . . . . . . . 10
|
24 | 18, 20, 23 | 3bitri 286 |
. . . . . . . . 9
|
25 | 2 | seqomlem1 7545 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . 15
|
27 | 26 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
28 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
29 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
30 | 28, 29 | opth1 4944 |
. . . . . . . . . . . . . 14
|
31 | 27, 30 | syl6bi 243 |
. . . . . . . . . . . . 13
|
32 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
33 | 32 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
34 | 33 | biimpd 219 |
. . . . . . . . . . . . 13
|
35 | 31, 34 | syli 39 |
. . . . . . . . . . . 12
|
36 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
37 | | vex 3203 |
. . . . . . . . . . . . . 14
|
38 | | vex 3203 |
. . . . . . . . . . . . . 14
|
39 | 37, 38 | op2nd 7177 |
. . . . . . . . . . . . 13
|
40 | 36, 39 | syl6req 2673 |
. . . . . . . . . . . 12
|
41 | 35, 40 | syl6 35 |
. . . . . . . . . . 11
|
42 | 41 | rexlimdva 3031 |
. . . . . . . . . 10
|
43 | 2 | seqomlem1 7545 |
. . . . . . . . . . . 12
|
44 | 32 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
45 | 44 | rspcev 3309 |
. . . . . . . . . . . 12
|
46 | 43, 45 | mpdan 702 |
. . . . . . . . . . 11
|
47 | | opeq2 4403 |
. . . . . . . . . . . . 13
|
48 | 47 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
49 | 48 | rexbidv 3052 |
. . . . . . . . . . 11
|
50 | 46, 49 | syl5ibrcom 237 |
. . . . . . . . . 10
|
51 | 42, 50 | impbid 202 |
. . . . . . . . 9
|
52 | 24, 51 | syl5bb 272 |
. . . . . . . 8
|
53 | 52 | alrimiv 1855 |
. . . . . . 7
|
54 | | fvex 6201 |
. . . . . . . 8
|
55 | | eqeq2 2633 |
. . . . . . . . . 10
|
56 | 55 | bibi2d 332 |
. . . . . . . . 9
|
57 | 56 | albidv 1849 |
. . . . . . . 8
|
58 | 54, 57 | spcev 3300 |
. . . . . . 7
|
59 | 53, 58 | syl 17 |
. . . . . 6
|
60 | | df-eu 2474 |
. . . . . 6
|
61 | 59, 60 | sylibr 224 |
. . . . 5
|
62 | 61 | rgen 2922 |
. . . 4
|
63 | | dff3 6372 |
. . . 4
|
64 | 17, 62, 63 | mpbir2an 955 |
. . 3
|
65 | | df-ima 5127 |
. . . 4
|
66 | 65 | feq1i 6036 |
. . 3
|
67 | 64, 66 | mpbir 221 |
. 2
|
68 | | dffn2 6047 |
. 2
|
69 | 67, 68 | mpbir 221 |
1
|