Description: Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | madeval2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | madeval | |
|
2 | scutcl | |
|
3 | eleq1 | |
|
4 | 3 | biimpd | |
5 | 2 4 | mpan9 | |
6 | 5 | rexlimivw | |
7 | 6 | rexlimivw | |
8 | 7 | pm4.71ri | |
9 | 8 | abbii | |
10 | eleq1 | |
|
11 | breq1 | |
|
12 | 10 11 | anbi12d | |
13 | 12 | rexxp | |
14 | imaindm | |
|
15 | dmscut | |
|
16 | 15 | ineq2i | |
17 | 16 | imaeq2i | |
18 | 14 17 | eqtri | |
19 | 18 | eleq2i | |
20 | vex | |
|
21 | 20 | elima | |
22 | elin | |
|
23 | 22 | anbi1i | |
24 | anass | |
|
25 | 23 24 | bitri | |
26 | 25 | rexbii2 | |
27 | 19 21 26 | 3bitri | |
28 | df-br | |
|
29 | 28 | anbi1i | |
30 | df-ov | |
|
31 | 30 | eqeq1i | |
32 | scutf | |
|
33 | ffn | |
|
34 | 32 33 | ax-mp | |
35 | fnbrfvb | |
|
36 | 34 35 | mpan | |
37 | 31 36 | syl5bb | |
38 | 37 | pm5.32i | |
39 | 29 38 | bitri | |
40 | 39 | 2rexbii | |
41 | 13 27 40 | 3bitr4i | |
42 | 41 | abbi2i | |
43 | df-rab | |
|
44 | 9 42 43 | 3eqtr4i | |
45 | 1 44 | eqtrdi | |