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

Metamath Proof Explorer

Theorem 1loopgrvd0

Description: The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
1loopgruspgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
1loopgruspgr.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
1loopgruspgr.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
1loopgrvd0.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) )
Assertion 1loopgrvd0 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2 1loopgruspgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 1loopgruspgr.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
4 1loopgruspgr.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5 1loopgrvd0.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) )
6 5 eldifbd ⊢ ( 𝜑 → ¬ 𝐾 ∈ { 𝑁 } )
7 snex ⊢ { 𝑁 } ∈ V
8 fvsng ⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝑁 } ∈ V ) → ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) = { 𝑁 } )
9 2 7 8 sylancl ⊢ ( 𝜑 → ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) = { 𝑁 } )
10 9 eleq2d ⊢ ( 𝜑 → ( 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ↔ 𝐾 ∈ { 𝑁 } ) )
11 6 10 mtbird ⊢ ( 𝜑 → ¬ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) )
12 4 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝑁 } ⟩ } )
13 dmsnopg ⊢ ( { 𝑁 } ∈ V → dom { ⟨ 𝐴 , { 𝑁 } ⟩ } = { 𝐴 } )
14 7 13 mp1i ⊢ ( 𝜑 → dom { ⟨ 𝐴 , { 𝑁 } ⟩ } = { 𝐴 } )
15 12 14 eqtrd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
16 4 fveq1d ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ) )
18 15 17 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ { 𝐴 } 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ) )
19 fveq2 ⊢ ( 𝑖 = 𝐴 → ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) = ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) )
20 19 eleq2d ⊢ ( 𝑖 = 𝐴 → ( 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
21 20 rexsng ⊢ ( 𝐴 ∈ 𝑋 → ( ∃ 𝑖 ∈ { 𝐴 } 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
22 2 21 syl ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ { 𝐴 } 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
23 18 22 bitrd ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
24 11 23 mtbird ⊢ ( 𝜑 → ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
25 5 eldifad ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
26 1 eleq2d ⊢ ( 𝜑 → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐾 ∈ 𝑉 ) )
27 25 26 mpbird ⊢ ( 𝜑 → 𝐾 ∈ ( Vtx ‘ 𝐺 ) )
28 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
30 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
31 28 29 30 vtxd0nedgb ⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
32 27 31 syl ⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
33 24 32 mpbird ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 )