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	$$⊢\phi \to G\mathrm{Struct}X$$
	structgrssvtx.v	$$⊢\phi \to V\in Y$$
	structgrssvtx.e	$$⊢\phi \to E\in Z$$
	structgrssvtx.s	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
Assertion	structgrssvtxlem	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	$$⊢\phi \to G\mathrm{Struct}X$$
2		structgrssvtx.v	$$⊢\phi \to V\in Y$$
3		structgrssvtx.e	$$⊢\phi \to E\in Z$$
4		structgrssvtx.s	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
5		fvexd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
6		fvexd	$$⊢\phi \to \mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
7		structex	$$⊢G\mathrm{Struct}X\to G\in \mathrm{V}$$
8	1 7	syl	$$⊢\phi \to G\in \mathrm{V}$$
9		slotsbaseefdif	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$$
10	9	a1i	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$$
11	5 6 2 3 8 10 4	hashdmpropge2	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$