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 e. NN
structvtxvallem.b 
|- ( Base ` ndx ) < S
structvtxvallem.g 
|- G = { <. ( Base ` ndx ) , V >. , <. S , E >. }
Assertion structvtxval 
|- ( ( V e. X /\ E e. Y ) -> ( Vtx ` G ) = V )

Proof

Step Hyp Ref Expression
1 structvtxvallem.s 
 |-  S e. NN
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 e. X /\ E e. Y ) -> G Struct <. ( Base ` ndx ) , S >. )
6 1 2 3 structvtxvallem 
 |-  ( ( V e. X /\ E e. Y ) -> 2 <_ ( # ` dom G ) )
7 simpl 
 |-  ( ( V e. X /\ E e. Y ) -> V e. X )
8 opex 
 |-  <. ( Base ` ndx ) , V >. e. _V
9 8 prid1 
 |-  <. ( Base ` ndx ) , V >. e. { <. ( Base ` ndx ) , V >. , <. S , E >. }
10 9 3 eleqtrri 
 |-  <. ( Base ` ndx ) , V >. e. G
11 10 a1i 
 |-  ( ( V e. X /\ E e. Y ) -> <. ( Base ` ndx ) , V >. e. G )
12 5 6 7 11 basvtxval 
 |-  ( ( V e. X /\ E e. Y ) -> ( Vtx ` G ) = V )