Description: Lemma for fmucnd . (Contributed by Thierry Arnoux, 19-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | fmucndlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ima | |
|
2 | simpr | |
|
3 | resmpo | |
|
4 | 2 3 | sylancom | |
5 | 4 | rneqd | |
6 | 1 5 | eqtrid | |
7 | vex | |
|
8 | vex | |
|
9 | 7 8 | op1std | |
10 | 9 | fveq2d | |
11 | 7 8 | op2ndd | |
12 | 11 | fveq2d | |
13 | 10 12 | opeq12d | |
14 | 13 | mpompt | |
15 | 14 | eqcomi | |
16 | 15 | rneqi | |
17 | fvexd | |
|
18 | fvexd | |
|
19 | 16 17 18 | fliftrel | |
20 | 19 | mptru | |
21 | 20 | sseli | |
22 | 21 | adantl | |
23 | xpss | |
|
24 | 23 | sseli | |
25 | 24 | adantl | |
26 | eqid | |
|
27 | opex | |
|
28 | 26 27 | elrnmpo | |
29 | eqcom | |
|
30 | fvex | |
|
31 | fvex | |
|
32 | 30 31 | opth2 | |
33 | 29 32 | bitri | |
34 | 33 | 2rexbii | |
35 | reeanv | |
|
36 | 28 34 35 | 3bitri | |
37 | fvelimab | |
|
38 | fvelimab | |
|
39 | 37 38 | anbi12d | |
40 | 36 39 | bitr4id | |
41 | opelxp | |
|
42 | 40 41 | bitr4di | |
43 | 42 | adantr | |
44 | 1st2nd2 | |
|
45 | 44 | adantl | |
46 | 45 | eleq1d | |
47 | 45 | eleq1d | |
48 | 43 46 47 | 3bitr4d | |
49 | 22 25 48 | eqrdav | |
50 | 6 49 | eqtrd | |