Step |
Hyp |
Ref |
Expression |
1 |
|
umgr2v2evtx.g |
⊢ 𝐺 = 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } 〉 |
2 |
1
|
fveq2i |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } 〉 ) |
3 |
|
simp1 |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑉 ∈ 𝑊 ) |
4 |
|
prex |
⊢ { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } ∈ V |
5 |
|
opiedgfv |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } ∈ V ) → ( iEdg ‘ 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } 〉 ) = { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } ) |
6 |
3 4 5
|
sylancl |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( iEdg ‘ 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } 〉 ) = { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } ) |
7 |
2 6
|
syl5eq |
⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( iEdg ‘ 𝐺 ) = { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } ) |