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	2strstr1	⊢ 𝐺 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 ‘ 𝐺 ) = 𝑉 )