Description: Lemma for ustuqtop . (Contributed by Thierry Arnoux, 11-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | utopustuq.1 | |
|
Assertion | ustuqtop5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | utopustuq.1 | |
|
2 | ustbasel | |
|
3 | snssi | |
|
4 | dfss | |
|
5 | 3 4 | sylib | |
6 | incom | |
|
7 | 5 6 | eqtr2di | |
8 | snnzg | |
|
9 | 7 8 | eqnetrd | |
10 | 9 | adantl | |
11 | xpima2 | |
|
12 | 10 11 | syl | |
13 | 12 | eqcomd | |
14 | imaeq1 | |
|
15 | 14 | rspceeqv | |
16 | 2 13 15 | syl2an2r | |
17 | elfvex | |
|
18 | 1 | ustuqtoplem | |
19 | 17 18 | mpidan | |
20 | 16 19 | mpbird | |