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	⊢ 𝑆 ∈ ℕ
	structvtxvallem.b	⊢ ( Base ‘ ndx ) < 𝑆
	structvtxvallem.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
Assertion	structvtxvallem	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 2 ≤ ( ♯ ‘ dom 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	⊢ 𝑆 ∈ ℕ
2		structvtxvallem.b	⊢ ( Base ‘ ndx ) < 𝑆
3		structvtxvallem.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
4		fvexd	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Base ‘ ndx ) ∈ V )
5	1	a1i	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝑆 ∈ ℕ )
6		simpl	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝑉 ∈ 𝑋 )
7		simpr	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐸 ∈ 𝑌 )
8		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ∈ V
9	3 8	eqeltri	⊢ 𝐺 ∈ V
10	9	a1i	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 ∈ V )
11		basendxnn	⊢ ( Base ‘ ndx ) ∈ ℕ
12	11	nnrei	⊢ ( Base ‘ ndx ) ∈ ℝ
13	12 2	ltneii	⊢ ( Base ‘ ndx ) ≠ 𝑆
14	13	a1i	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Base ‘ ndx ) ≠ 𝑆 )
15	3	eqimss2i	⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ⊆ 𝐺
16	15	a1i	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ } ⊆ 𝐺 )
17	4 5 6 7 10 14 16	hashdmpropge2	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 2 ≤ ( ♯ ‘ dom 𝐺 ) )