| Step |
Hyp |
Ref |
Expression |
| 1 |
|
p1evtxdeq.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
| 2 |
|
p1evtxdeq.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
| 3 |
|
p1evtxdeq.f |
⊢ ( 𝜑 → Fun 𝐼 ) |
| 4 |
|
p1evtxdeq.fv |
⊢ ( 𝜑 → ( Vtx ‘ 𝐹 ) = 𝑉 ) |
| 5 |
|
p1evtxdeq.fi |
⊢ ( 𝜑 → ( iEdg ‘ 𝐹 ) = ( 𝐼 ∪ { ⟨ 𝐾 , 𝐸 ⟩ } ) ) |
| 6 |
|
p1evtxdeq.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑋 ) |
| 7 |
|
p1evtxdeq.d |
⊢ ( 𝜑 → 𝐾 ∉ dom 𝐼 ) |
| 8 |
|
p1evtxdeq.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
| 9 |
|
p1evtxdeq.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝑌 ) |
| 10 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
| 11 |
|
snex |
⊢ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V |
| 12 |
10 11
|
pm3.2i |
⊢ ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) |
| 13 |
|
opiedgfv |
⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = { ⟨ 𝐾 , 𝐸 ⟩ } ) |
| 14 |
13
|
eqcomd |
⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → { ⟨ 𝐾 , 𝐸 ⟩ } = ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ) |
| 15 |
12 14
|
ax-mp |
⊢ { ⟨ 𝐾 , 𝐸 ⟩ } = ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) |
| 16 |
|
opvtxfv |
⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = 𝑉 ) |
| 17 |
12 16
|
mp1i |
⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = 𝑉 ) |
| 18 |
|
dmsnopg |
⊢ ( 𝐸 ∈ 𝑌 → dom { ⟨ 𝐾 , 𝐸 ⟩ } = { 𝐾 } ) |
| 19 |
9 18
|
syl |
⊢ ( 𝜑 → dom { ⟨ 𝐾 , 𝐸 ⟩ } = { 𝐾 } ) |
| 20 |
19
|
ineq2d |
⊢ ( 𝜑 → ( dom 𝐼 ∩ dom { ⟨ 𝐾 , 𝐸 ⟩ } ) = ( dom 𝐼 ∩ { 𝐾 } ) ) |
| 21 |
|
df-nel |
⊢ ( 𝐾 ∉ dom 𝐼 ↔ ¬ 𝐾 ∈ dom 𝐼 ) |
| 22 |
7 21
|
sylib |
⊢ ( 𝜑 → ¬ 𝐾 ∈ dom 𝐼 ) |
| 23 |
|
disjsn |
⊢ ( ( dom 𝐼 ∩ { 𝐾 } ) = ∅ ↔ ¬ 𝐾 ∈ dom 𝐼 ) |
| 24 |
22 23
|
sylibr |
⊢ ( 𝜑 → ( dom 𝐼 ∩ { 𝐾 } ) = ∅ ) |
| 25 |
20 24
|
eqtrd |
⊢ ( 𝜑 → ( dom 𝐼 ∩ dom { ⟨ 𝐾 , 𝐸 ⟩ } ) = ∅ ) |
| 26 |
|
funsng |
⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → Fun { ⟨ 𝐾 , 𝐸 ⟩ } ) |
| 27 |
6 9 26
|
syl2anc |
⊢ ( 𝜑 → Fun { ⟨ 𝐾 , 𝐸 ⟩ } ) |
| 28 |
2 15 1 17 4 25 3 27 8 5
|
vtxdun |
⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) ) |