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

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

Metamath Proof Explorer