Description: Lemma 2 for fundcmpsurinj . (Contributed by AV, 4-Mar-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fundcmpsurinj.p | |
|
fundcmpsurinj.g | |
||
Assertion | fundcmpsurinjlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fundcmpsurinj.p | |
|
2 | fundcmpsurinj.g | |
|
3 | fnex | |
|
4 | cnvexg | |
|
5 | imaexg | |
|
6 | 3 4 5 | 3syl | |
7 | 6 | ralrimivw | |
8 | 2 | fnmpt | |
9 | 7 8 | syl | |
10 | 1 2 | fundcmpsurinjlem1 | |
11 | df-fo | |
|
12 | 9 10 11 | sylanblrc | |