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

Metamath Proof Explorer

Theorem structvtxval

Description: The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypotheses structvtxvallem.s ⊢ 𝑆 ∈ ℕ
structvtxvallem.b ⊢ ( Base ‘ ndx ) < 𝑆
structvtxvallem.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
Assertion structvtxval ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 structvtxvallem.s ⊢ 𝑆 ∈ ℕ
2 structvtxvallem.b ⊢ ( Base ‘ ndx ) < 𝑆
3 structvtxvallem.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
4 3 2 1 2strstr ⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩
5 4 a1i ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑆 ⟩ )
6 1 2 3 structvtxvallem ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
7 simpl ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝑉 ∈ 𝑋 )
8 opex ⊢ ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ V
9 8 prid1 ⊢ ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ 𝑆 , 𝐸 ⟩ }
10 9 3 eleqtrri ⊢ ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺
11 10 a1i ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 )
12 5 6 7 11 basvtxval ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )