Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by Mario Carneiro, 23-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cygzn.b | |
|
cygzn.n | |
||
cygzn.y | |
||
cygzn.m | |
||
cygzn.l | |
||
cygzn.e | |
||
cygzn.g | |
||
cygzn.x | |
||
cygzn.f | |
||
Assertion | cygznlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cygzn.b | |
|
2 | cygzn.n | |
|
3 | cygzn.y | |
|
4 | cygzn.m | |
|
5 | cygzn.l | |
|
6 | cygzn.e | |
|
7 | cygzn.g | |
|
8 | cygzn.x | |
|
9 | cygzn.f | |
|
10 | fvexd | |
|
11 | ovexd | |
|
12 | fveq2 | |
|
13 | oveq1 | |
|
14 | 1 2 3 4 5 6 7 8 9 | cygznlem2a | |
15 | 14 | ffund | |
16 | 9 10 11 12 13 15 | fliftval | |