Step |
Hyp |
Ref |
Expression |
1 |
|
isumgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
isumgr.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
1 2
|
umgrf |
⊢ ( 𝐺 ∈ UMGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
4 |
3
|
ffvelrnda |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
5 |
|
fveqeq2 |
⊢ ( 𝑥 = ( 𝐸 ‘ 𝑋 ) → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) ) |
6 |
5
|
elrab |
⊢ ( ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( 𝐸 ‘ 𝑋 ) ∈ 𝒫 𝑉 ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) ) |
7 |
6
|
simprbi |
⊢ ( ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) |
8 |
4 7
|
syl |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) |