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\in \mathbb{N}$$
	structvtxvallem.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<S$$
	structvtxvallem.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
Assertion	structvtxvallem	$$⊢\left(V\in X\wedge E\in Y\right)\to 2\le \left|\mathrm{dom}G\right|$$

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	$$⊢S\in \mathbb{N}$$
2		structvtxvallem.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<S$$
3		structvtxvallem.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
4		fvexd	$$⊢\left(V\in X\wedge E\in Y\right)\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
5	1	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to S\in \mathbb{N}$$
6		simpl	$$⊢\left(V\in X\wedge E\in Y\right)\to V\in X$$
7		simpr	$$⊢\left(V\in X\wedge E\in Y\right)\to E\in Y$$
8		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\in \mathrm{V}$$
9	3 8	eqeltri	$$⊢G\in \mathrm{V}$$
10	9	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to G\in \mathrm{V}$$
11		basendxnn	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathbb{N}$$
12	11	nnrei	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in ℝ$$
13	12 2	ltneii	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne S$$
14	13	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to {\mathrm{Base}}_{\mathrm{ndx}}\ne S$$
15	3	eqimss2i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\subseteq G$$
16	15	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\subseteq G$$
17	4 5 6 7 10 14 16	hashdmpropge2	$$⊢\left(V\in X\wedge E\in Y\right)\to 2\le \left|\mathrm{dom}G\right|$$