Theorem structvtxvallem

Description: Lemma for structvtxval and structiedg0val . (Contributed by AV, 23-Sep-2020) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	structvtxvallem.s	|- S e. NN
	structvtxvallem.b	|- ( Base ` ndx ) < S
	structvtxvallem.g	|- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }
Assertion	structvtxvallem	|- ( ( V e. X /\ E e. Y ) -> 2 <_ ( # ` dom G ) )

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	|- S e. NN
2		structvtxvallem.b	|- ( Base ` ndx ) < S
3		structvtxvallem.g	|- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }
4		fvexd	|- ( ( V e. X /\ E e. Y ) -> ( Base ` ndx ) e. _V )
5	1	a1i	|- ( ( V e. X /\ E e. Y ) -> S e. NN )
6		simpl	|- ( ( V e. X /\ E e. Y ) -> V e. X )
7		simpr	|- ( ( V e. X /\ E e. Y ) -> E e. Y )
8		prex	|- { <. ( Base ` ndx ) , V >. , <. S , E >. } e. _V
9	3 8	eqeltri	|- G e. _V
10	9	a1i	|- ( ( V e. X /\ E e. Y ) -> G e. _V )
11		basendxnn	|- ( Base ` ndx ) e. NN
12	11	nnrei	|- ( Base ` ndx ) e. RR
13	12 2	ltneii	|- ( Base ` ndx ) =/= S
14	13	a1i	|- ( ( V e. X /\ E e. Y ) -> ( Base ` ndx ) =/= S )
15	3	eqimss2i	|- { <. ( Base ` ndx ) , V >. , <. S , E >. } C_ G
16	15	a1i	|- ( ( V e. X /\ E e. Y ) -> { <. ( Base ` ndx ) , V >. , <. S , E >. } C_ G )
17	4 5 6 7 10 14 16	hashdmpropge2	|- ( ( V e. X /\ E e. Y ) -> 2 <_ ( # ` dom G ) )