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