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

Metamath Proof Explorer

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