Step |
Hyp |
Ref |
Expression |
1 |
|
isupgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
isupgr.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
1 2
|
upgrf |
⊢ ( 𝐺 ∈ UPGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |
4 |
|
fndm |
⊢ ( 𝐸 Fn 𝐴 → dom 𝐸 = 𝐴 ) |
5 |
4
|
feq2d |
⊢ ( 𝐸 Fn 𝐴 → ( 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ 𝐸 : 𝐴 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
6 |
3 5
|
syl5ibcom |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐸 Fn 𝐴 → 𝐸 : 𝐴 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) ) |
7 |
6
|
imp |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ) → 𝐸 : 𝐴 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) |