This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 basendxnedgfndx ⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
10 9 a1i ⊢ ( 𝜑 → ( Base ‘ ndx ) ≠ ( .ef ‘ ndx ) )
11 5 6 2 3 8 10 4 hashdmpropge2 ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )