Metamath Proof Explorer


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 𝐺 ) )