Description: Lemma 4 for vtxdginducedm1 . (Contributed by AV, 17-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vtxdginducedm1.v | |
|
vtxdginducedm1.e | |
||
vtxdginducedm1.k | |
||
vtxdginducedm1.i | |
||
vtxdginducedm1.p | |
||
vtxdginducedm1.s | |
||
vtxdginducedm1.j | |
||
Assertion | vtxdginducedm1lem4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtxdginducedm1.v | |
|
2 | vtxdginducedm1.e | |
|
3 | vtxdginducedm1.k | |
|
4 | vtxdginducedm1.i | |
|
5 | vtxdginducedm1.p | |
|
6 | vtxdginducedm1.s | |
|
7 | vtxdginducedm1.j | |
|
8 | fveq2 | |
|
9 | 8 | eleq2d | |
10 | 9 7 | elrab2 | |
11 | eldifsn | |
|
12 | df-ne | |
|
13 | eleq2 | |
|
14 | elsni | |
|
15 | 14 | eqcomd | |
16 | 13 15 | syl6bi | |
17 | 16 | com12 | |
18 | 17 | con3rr3 | |
19 | 12 18 | sylbi | |
20 | 11 19 | simplbiim | |
21 | 20 | com12 | |
22 | 10 21 | simplbiim | |
23 | 22 | impcom | |
24 | 23 | ralrimiva | |
25 | rabeq0 | |
|
26 | 24 25 | sylibr | |
27 | 2 | fvexi | |
28 | 27 | dmex | |
29 | 7 28 | rab2ex | |
30 | hasheq0 | |
|
31 | 29 30 | ax-mp | |
32 | 26 31 | sylibr | |