Step |
Hyp |
Ref |
Expression |
1 |
|
basvtxval.s |
⊢ ( 𝜑 → 𝐺 Struct 𝑋 ) |
2 |
|
basvtxval.d |
⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) ) |
3 |
|
basvtxval.v |
⊢ ( 𝜑 → 𝑉 ∈ 𝑌 ) |
4 |
|
basvtxval.b |
⊢ ( 𝜑 → 〈 ( Base ‘ ndx ) , 𝑉 〉 ∈ 𝐺 ) |
5 |
|
structn0fun |
⊢ ( 𝐺 Struct 𝑋 → Fun ( 𝐺 ∖ { ∅ } ) ) |
6 |
1 5
|
syl |
⊢ ( 𝜑 → Fun ( 𝐺 ∖ { ∅ } ) ) |
7 |
|
funvtxdmge2val |
⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) ) |
8 |
6 2 7
|
syl2anc |
⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = ( Base ‘ 𝐺 ) ) |
9 |
1 3 4
|
opelstrbas |
⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝐺 ) ) |
10 |
8 9
|
eqtr4d |
⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 ) |