This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem p1evtxdeqlem

Description: Lemma for p1evtxdeq and p1evtxdp1 . (Contributed by AV, 3-Mar-2021)

Ref Expression
Hypotheses p1evtxdeq.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
p1evtxdeq.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
p1evtxdeq.f ⊢ ( 𝜑 → Fun 𝐼 )
p1evtxdeq.fv ⊢ ( 𝜑 → ( Vtx ‘ 𝐹 ) = 𝑉 )
p1evtxdeq.fi ⊢ ( 𝜑 → ( iEdg ‘ 𝐹 ) = ( 𝐼 ∪ { ⟨ 𝐾 , 𝐸 ⟩ } ) )
p1evtxdeq.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
p1evtxdeq.d ⊢ ( 𝜑 → 𝐾 ∉ dom 𝐼 )
p1evtxdeq.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
p1evtxdeq.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
Assertion p1evtxdeqlem ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) )

Proof

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 ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) )