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	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
	structgrssvtx.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
	structgrssvtx.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑍 )
	structgrssvtx.s	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
Assertion	structgrssvtxlem	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
2		structgrssvtx.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
3		structgrssvtx.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑍 )
4		structgrssvtx.s	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
5		fvexd	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ V )
6		fvexd	⊢ ( 𝜑 → ( .ef ‘ ndx ) ∈ V )
7		structex	⊢ ( 𝐺 Struct 𝑋 → 𝐺 ∈ V )
8	1 7	syl	⊢ ( 𝜑 → 𝐺 ∈ V )
9		slotsbaseefdif	⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
10	9	a1i	⊢ ( 𝜑 → ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) )
11	5 6 2 3 8 10 4	hashdmpropge2	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )