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	2strstr1	|- 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 )