Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | 2ndconst | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snnzg | |
|
2 | fo2ndres | |
|
3 | 1 2 | syl | |
4 | moeq | |
|
5 | 4 | moani | |
6 | vex | |
|
7 | 6 | brresi | |
8 | fo2nd | |
|
9 | fofn | |
|
10 | 8 9 | ax-mp | |
11 | vex | |
|
12 | fnbrfvb | |
|
13 | 10 11 12 | mp2an | |
14 | 13 | anbi2i | |
15 | elxp7 | |
|
16 | eleq1 | |
|
17 | 16 | biimpac | |
18 | 17 | adantll | |
19 | 18 | adantll | |
20 | elsni | |
|
21 | eqopi | |
|
22 | 21 | anassrs | |
23 | 20 22 | sylanl2 | |
24 | 23 | adantlrr | |
25 | 19 24 | jca | |
26 | 15 25 | sylanb | |
27 | 26 | adantl | |
28 | simprr | |
|
29 | snidg | |
|
30 | 29 | adantr | |
31 | simprl | |
|
32 | 30 31 | opelxpd | |
33 | 28 32 | eqeltrd | |
34 | fveq2 | |
|
35 | op2ndg | |
|
36 | 35 | elvd | |
37 | 34 36 | sylan9eqr | |
38 | 37 | adantrl | |
39 | 33 38 | jca | |
40 | 27 39 | impbida | |
41 | 14 40 | bitr3id | |
42 | 7 41 | bitrid | |
43 | 42 | mobidv | |
44 | 5 43 | mpbiri | |
45 | 44 | alrimiv | |
46 | funcnv2 | |
|
47 | 45 46 | sylibr | |
48 | dff1o3 | |
|
49 | 3 47 48 | sylanbrc | |