Description: Lemma for ustuqtop . (Contributed by Thierry Arnoux, 11-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | utopustuq.1 | |
|
Assertion | ustuqtoplem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | utopustuq.1 | |
|
2 | simpl | |
|
3 | 2 | sneqd | |
4 | 3 | imaeq2d | |
5 | 4 | mpteq2dva | |
6 | 5 | rneqd | |
7 | 6 | cbvmptv | |
8 | 1 7 | eqtri | |
9 | simpr2 | |
|
10 | 9 | sneqd | |
11 | 10 | imaeq2d | |
12 | 11 | 3anassrs | |
13 | 12 | mpteq2dva | |
14 | 13 | rneqd | |
15 | simpr | |
|
16 | mptexg | |
|
17 | rnexg | |
|
18 | 16 17 | syl | |
19 | 18 | adantr | |
20 | 8 14 15 19 | fvmptd2 | |
21 | 20 | eleq2d | |
22 | imaeq1 | |
|
23 | 22 | cbvmptv | |
24 | 23 | elrnmpt | |
25 | 21 24 | sylan9bb | |