Step |
Hyp |
Ref |
Expression |
1 |
|
structgrssvtx.g |
⊢ ( 𝜑 → 𝐺 Struct 𝑋 ) |
2 |
|
structgrssvtx.v |
⊢ ( 𝜑 → 𝑉 ∈ 𝑌 ) |
3 |
|
structgrssvtx.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝑍 ) |
4 |
|
structgrssvtx.s |
⊢ ( 𝜑 → { 〈 ( Base ‘ ndx ) , 𝑉 〉 , 〈 ( .ef ‘ ndx ) , 𝐸 〉 } ⊆ 𝐺 ) |
5 |
1 2 3 4
|
structgrssvtxlem |
⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) ) |
6 |
|
opex |
⊢ 〈 ( Base ‘ ndx ) , 𝑉 〉 ∈ V |
7 |
|
opex |
⊢ 〈 ( .ef ‘ ndx ) , 𝐸 〉 ∈ V |
8 |
6 7
|
prss |
⊢ ( ( 〈 ( Base ‘ ndx ) , 𝑉 〉 ∈ 𝐺 ∧ 〈 ( .ef ‘ ndx ) , 𝐸 〉 ∈ 𝐺 ) ↔ { 〈 ( Base ‘ ndx ) , 𝑉 〉 , 〈 ( .ef ‘ ndx ) , 𝐸 〉 } ⊆ 𝐺 ) |
9 |
|
simpr |
⊢ ( ( 〈 ( Base ‘ ndx ) , 𝑉 〉 ∈ 𝐺 ∧ 〈 ( .ef ‘ ndx ) , 𝐸 〉 ∈ 𝐺 ) → 〈 ( .ef ‘ ndx ) , 𝐸 〉 ∈ 𝐺 ) |
10 |
8 9
|
sylbir |
⊢ ( { 〈 ( Base ‘ ndx ) , 𝑉 〉 , 〈 ( .ef ‘ ndx ) , 𝐸 〉 } ⊆ 𝐺 → 〈 ( .ef ‘ ndx ) , 𝐸 〉 ∈ 𝐺 ) |
11 |
4 10
|
syl |
⊢ ( 𝜑 → 〈 ( .ef ‘ ndx ) , 𝐸 〉 ∈ 𝐺 ) |
12 |
1 5 3 11
|
edgfiedgval |
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = 𝐸 ) |