Description: Lemma for p1evtxdeq and p1evtxdp1 . (Contributed by AV, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | p1evtxdeq.v | |
|
p1evtxdeq.i | |
||
p1evtxdeq.f | |
||
p1evtxdeq.fv | |
||
p1evtxdeq.fi | |
||
p1evtxdeq.k | |
||
p1evtxdeq.d | |
||
p1evtxdeq.u | |
||
p1evtxdeq.e | |
||
Assertion | p1evtxdeqlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | p1evtxdeq.v | |
|
2 | p1evtxdeq.i | |
|
3 | p1evtxdeq.f | |
|
4 | p1evtxdeq.fv | |
|
5 | p1evtxdeq.fi | |
|
6 | p1evtxdeq.k | |
|
7 | p1evtxdeq.d | |
|
8 | p1evtxdeq.u | |
|
9 | p1evtxdeq.e | |
|
10 | 1 | fvexi | |
11 | snex | |
|
12 | 10 11 | pm3.2i | |
13 | opiedgfv | |
|
14 | 13 | eqcomd | |
15 | 12 14 | ax-mp | |
16 | opvtxfv | |
|
17 | 12 16 | mp1i | |
18 | dmsnopg | |
|
19 | 9 18 | syl | |
20 | 19 | ineq2d | |
21 | df-nel | |
|
22 | 7 21 | sylib | |
23 | disjsn | |
|
24 | 22 23 | sylibr | |
25 | 20 24 | eqtrd | |
26 | funsng | |
|
27 | 6 9 26 | syl2anc | |
28 | 2 15 1 17 4 25 3 27 8 5 | vtxdun | |