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	|- ( ph -> G Struct X )
	structgrssvtx.v	|- ( ph -> V e. Y )
	structgrssvtx.e	|- ( ph -> E e. Z )
	structgrssvtx.s	|- ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
Assertion	structgrssvtxlem	|- ( ph -> 2 <_ ( # ` dom G ) )

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	|- ( ph -> G Struct X )
2		structgrssvtx.v	|- ( ph -> V e. Y )
3		structgrssvtx.e	|- ( ph -> E e. Z )
4		structgrssvtx.s	|- ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
5		fvexd	|- ( ph -> ( Base ` ndx ) e. _V )
6		fvexd	|- ( ph -> ( .ef ` ndx ) e. _V )
7		structex	|- ( G Struct X -> G e. _V )
8	1 7	syl	|- ( ph -> G e. _V )
9		slotsbaseefdif	|- ( Base ` ndx ) =/= ( .ef ` ndx )
10	9	a1i	|- ( ph -> ( Base ` ndx ) =/= ( .ef ` ndx ) )
11	5 6 2 3 8 10 4	hashdmpropge2	|- ( ph -> 2 <_ ( # ` dom G ) )