Description: The value of the function F . (Contributed by Mario Carneiro, 23-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | flift.1 | |
|
flift.2 | |
||
flift.3 | |
||
fliftval.4 | |
||
fliftval.5 | |
||
fliftval.6 | |
||
Assertion | fliftval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flift.1 | |
|
2 | flift.2 | |
|
3 | flift.3 | |
|
4 | fliftval.4 | |
|
5 | fliftval.5 | |
|
6 | fliftval.6 | |
|
7 | 6 | adantr | |
8 | simpr | |
|
9 | eqidd | |
|
10 | eqidd | |
|
11 | 9 10 | anim12ci | |
12 | 4 | eqeq2d | |
13 | 5 | eqeq2d | |
14 | 12 13 | anbi12d | |
15 | 14 | rspcev | |
16 | 8 11 15 | syl2anc | |
17 | 1 2 3 | fliftel | |
18 | 17 | adantr | |
19 | 16 18 | mpbird | |
20 | funbrfv | |
|
21 | 7 19 20 | sylc | |