Metamath Proof Explorer


Theorem structgrssvtxlem

Description: Lemma for structgrssvtx and structgrssiedg . (Contributed by AV, 14-Oct-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypotheses structgrssvtx.g φ G Struct X
structgrssvtx.v φ V Y
structgrssvtx.e φ E Z
structgrssvtx.s φ Base ndx V ef ndx E G
Assertion structgrssvtxlem φ 2 dom G

Proof

Step Hyp Ref Expression
1 structgrssvtx.g φ G Struct X
2 structgrssvtx.v φ V Y
3 structgrssvtx.e φ E Z
4 structgrssvtx.s φ Base ndx V ef ndx E G
5 fvexd φ Base ndx V
6 fvexd φ ef ndx V
7 structex G Struct X G V
8 1 7 syl φ G V
9 slotsbaseefdif Base ndx ef ndx
10 9 a1i φ Base ndx ef ndx
11 5 6 2 3 8 10 4 hashdmpropge2 φ 2 dom G