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 ⊢ S ∈ ℕ
structvtxvallem.b ⊢ Base ndx < S
structvtxvallem.g ⊢ G = Base ndx V S E
Assertion structvtxval ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ G = V

Proof

Step Hyp Ref Expression
1 structvtxvallem.s ⊢ S ∈ ℕ
2 structvtxvallem.b ⊢ Base ndx < S
3 structvtxvallem.g ⊢ G = Base ndx V S E
4 3 2 1 2strstr ⊢ G Struct Base ndx S
5 4 a1i ⊢ V ∈ X ∧ E ∈ Y → G Struct Base ndx S
6 1 2 3 structvtxvallem ⊢ V ∈ X ∧ E ∈ Y → 2 ≤ dom ⁡ G
7 simpl ⊢ V ∈ X ∧ E ∈ Y → V ∈ X
8 opex ⊢ Base ndx V ∈ V
9 8 prid1 ⊢ Base ndx V ∈ Base ndx V S E
10 9 3 eleqtrri ⊢ Base ndx V ∈ G
11 10 a1i ⊢ V ∈ X ∧ E ∈ Y → Base ndx V ∈ G
12 5 6 7 11 basvtxval ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ G = V