Description: An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017) (Proof shortened by Alexander van der Vekens, 16-Dec-2017) (Revised by AV, 15-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | usgredgop | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 = ( iEdg ‘ 𝐺 ) ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ↔ 〈 𝑋 , { 𝑀 , 𝑁 } 〉 ∈ 𝐸 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | usgrfun | ⊢ ( 𝐺 ∈ USGraph → Fun ( iEdg ‘ 𝐺 ) ) | |
2 | funeq | ⊢ ( 𝐸 = ( iEdg ‘ 𝐺 ) → ( Fun 𝐸 ↔ Fun ( iEdg ‘ 𝐺 ) ) ) | |
3 | 1 2 | syl5ibrcom | ⊢ ( 𝐺 ∈ USGraph → ( 𝐸 = ( iEdg ‘ 𝐺 ) → Fun 𝐸 ) ) |
4 | 3 | imp | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 = ( iEdg ‘ 𝐺 ) ) → Fun 𝐸 ) |
5 | funopfvb | ⊢ ( ( Fun 𝐸 ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ↔ 〈 𝑋 , { 𝑀 , 𝑁 } 〉 ∈ 𝐸 ) ) | |
6 | 4 5 | stoic3 | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐸 = ( iEdg ‘ 𝐺 ) ∧ 𝑋 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ↔ 〈 𝑋 , { 𝑀 , 𝑁 } 〉 ∈ 𝐸 ) ) |