Description: Lemma for poimir establishing existence for poimirlem18 . (Contributed by Brendan Leahy, 21-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | poimir.0 | |
|
poimirlem22.s | |
||
poimirlem22.1 | |
||
poimirlem22.2 | |
||
poimirlem18.3 | |
||
poimirlem18.4 | |
||
Assertion | poimirlem17 | |