Description: Lemma 1 for mapfien . (Contributed by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mapfien.s | |
|
mapfien.t | |
||
mapfien.w | |
||
mapfien.f | |
||
mapfien.g | |
||
mapfien.a | |
||
mapfien.b | |
||
mapfien.c | |
||
mapfien.d | |
||
mapfien.z | |
||
Assertion | mapfienlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mapfien.s | |
|
2 | mapfien.t | |
|
3 | mapfien.w | |
|
4 | mapfien.f | |
|
5 | mapfien.g | |
|
6 | mapfien.a | |
|
7 | mapfien.b | |
|
8 | mapfien.c | |
|
9 | mapfien.d | |
|
10 | mapfien.z | |
|
11 | 3 | fvexi | |
12 | 11 | a1i | |
13 | 10 | adantr | |
14 | elrabi | |
|
15 | elmapi | |
|
16 | 14 15 | syl | |
17 | 16 1 | eleq2s | |
18 | f1of | |
|
19 | 4 18 | syl | |
20 | fco | |
|
21 | 17 19 20 | syl2anr | |
22 | f1of | |
|
23 | 5 22 | syl | |
24 | 23 | adantr | |
25 | ssidd | |
|
26 | 8 | adantr | |
27 | 7 | adantr | |
28 | breq1 | |
|
29 | 28 1 | elrab2 | |
30 | 29 | simprbi | |
31 | 30 | adantl | |
32 | f1of1 | |
|
33 | 4 32 | syl | |
34 | 33 | adantr | |
35 | simpr | |
|
36 | 31 34 13 35 | fsuppco | |
37 | 3 | eqcomi | |
38 | 37 | a1i | |
39 | 12 13 21 24 25 26 27 36 38 | fsuppcor | |