Description: Lemma for smfpimcc given the choice function C . (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | smfpimcclem.n | |
|
smfpimcclem.z | |
||
smfpimcclem.s | |
||
smfpimcclem.c | |
||
smfpimcclem.h | |
||
Assertion | smfpimcclem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | smfpimcclem.n | |
|
2 | smfpimcclem.z | |
|
3 | smfpimcclem.s | |
|
4 | smfpimcclem.c | |
|
5 | smfpimcclem.h | |
|
6 | nfcv | |
|
7 | 6 | ssrab2f | |
8 | eqid | |
|
9 | 8 3 | rabexd | |
10 | 9 | adantr | |
11 | simpl | |
|
12 | simpr | |
|
13 | eqid | |
|
14 | 13 | elrnmpt1 | |
15 | 12 10 14 | syl2anc | |
16 | 11 15 | jca | |
17 | eleq1 | |
|
18 | 17 | anbi2d | |
19 | fveq2 | |
|
20 | id | |
|
21 | 19 20 | eleq12d | |
22 | 18 21 | imbi12d | |
23 | 22 4 | vtoclg | |
24 | 10 16 23 | sylc | |
25 | 7 24 | sselid | |
26 | 1 25 5 | fmptdf | |
27 | nfcv | |
|
28 | nfrab1 | |
|
29 | 27 28 | nffv | |
30 | nfcv | |
|
31 | nfcv | |
|
32 | 29 31 | nfin | |
33 | 30 32 | nfeq | |
34 | ineq1 | |
|
35 | 34 | eqeq2d | |
36 | 29 6 33 35 | elrabf | |
37 | 24 36 | sylib | |
38 | 37 | simprd | |
39 | 5 | a1i | |
40 | 24 | elexd | |
41 | 39 40 | fvmpt2d | |
42 | 41 | ineq1d | |
43 | 38 42 | eqtr4d | |
44 | 43 | ex | |
45 | 1 44 | ralrimi | |
46 | 2 | elexi | |
47 | 46 | mptex | |
48 | 5 47 | eqeltri | |
49 | feq1 | |
|
50 | nfcv | |
|
51 | nfmpt1 | |
|
52 | 5 51 | nfcxfr | |
53 | 50 52 | nfeq | |
54 | fveq1 | |
|
55 | 54 | ineq1d | |
56 | 55 | eqeq2d | |
57 | 53 56 | ralbid | |
58 | 49 57 | anbi12d | |
59 | 48 58 | spcev | |
60 | 26 45 59 | syl2anc | |