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

Metamath Proof Explorer

Theorem 1egrvtxdg0

Description: The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1egrvtxdg1.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
1egrvtxdg1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
1egrvtxdg1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
1egrvtxdg1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
1egrvtxdg1.n ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
1egrvtxdg0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
1egrvtxdg0.n ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
1egrvtxdg0.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } )
Assertion 1egrvtxdg0 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 )

Proof

Step Hyp Ref Expression
1 1egrvtxdg1.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2 1egrvtxdg1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 1egrvtxdg1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4 1egrvtxdg1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 1egrvtxdg1.n ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
6 1egrvtxdg0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
7 1egrvtxdg0.n ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
8 1egrvtxdg0.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } )
9 1 adantl ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )
10 2 adantl ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → 𝐴 ∈ 𝑋 )
11 3 adantl ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → 𝐵 ∈ 𝑉 )
12 8 adantl ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } )
13 preq2 ⊢ ( 𝐷 = 𝐵 → { 𝐵 , 𝐷 } = { 𝐵 , 𝐵 } )
14 13 eqcoms ⊢ ( 𝐵 = 𝐷 → { 𝐵 , 𝐷 } = { 𝐵 , 𝐵 } )
15 dfsn2 ⊢ { 𝐵 } = { 𝐵 , 𝐵 }
16 14 15 eqtr4di ⊢ ( 𝐵 = 𝐷 → { 𝐵 , 𝐷 } = { 𝐵 } )
17 16 adantr ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → { 𝐵 , 𝐷 } = { 𝐵 } )
18 17 opeq2d ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ = ⟨ 𝐴 , { 𝐵 } ⟩ )
19 18 sneqd ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } = { ⟨ 𝐴 , { 𝐵 } ⟩ } )
20 12 19 eqtrd ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 } ⟩ } )
21 5 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
22 4 21 jca ⊢ ( 𝜑 → ( 𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐵 ) )
23 eldifsn ⊢ ( 𝐶 ∈ ( 𝑉 ∖ { 𝐵 } ) ↔ ( 𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐵 ) )
24 22 23 sylibr ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑉 ∖ { 𝐵 } ) )
25 24 adantl ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → 𝐶 ∈ ( 𝑉 ∖ { 𝐵 } ) )
26 9 10 11 20 25 1loopgrvd0 ⊢ ( ( 𝐵 = 𝐷 ∧ 𝜑 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 )
27 26 ex ⊢ ( 𝐵 = 𝐷 → ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 ) )
28 necom ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
29 df-ne ⊢ ( 𝐶 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐵 )
30 28 29 sylbb ⊢ ( 𝐵 ≠ 𝐶 → ¬ 𝐶 = 𝐵 )
31 5 30 syl ⊢ ( 𝜑 → ¬ 𝐶 = 𝐵 )
32 7 neneqd ⊢ ( 𝜑 → ¬ 𝐶 = 𝐷 )
33 31 32 jca ⊢ ( 𝜑 → ( ¬ 𝐶 = 𝐵 ∧ ¬ 𝐶 = 𝐷 ) )
34 33 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( ¬ 𝐶 = 𝐵 ∧ ¬ 𝐶 = 𝐷 ) )
35 ioran ⊢ ( ¬ ( 𝐶 = 𝐵 ∨ 𝐶 = 𝐷 ) ↔ ( ¬ 𝐶 = 𝐵 ∧ ¬ 𝐶 = 𝐷 ) )
36 34 35 sylibr ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ¬ ( 𝐶 = 𝐵 ∨ 𝐶 = 𝐷 ) )
37 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
38 8 rneqd ⊢ ( 𝜑 → ran ( iEdg ‘ 𝐺 ) = ran { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } )
39 rnsnopg ⊢ ( 𝐴 ∈ 𝑋 → ran { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } = { { 𝐵 , 𝐷 } } )
40 2 39 syl ⊢ ( 𝜑 → ran { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } = { { 𝐵 , 𝐷 } } )
41 38 40 eqtrd ⊢ ( 𝜑 → ran ( iEdg ‘ 𝐺 ) = { { 𝐵 , 𝐷 } } )
42 37 41 eqtrid ⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝐵 , 𝐷 } } )
43 42 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( Edg ‘ 𝐺 ) = { { 𝐵 , 𝐷 } } )
44 43 rexeqdv ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝐶 ∈ 𝑒 ↔ ∃ 𝑒 ∈ { { 𝐵 , 𝐷 } } 𝐶 ∈ 𝑒 ) )
45 prex ⊢ { 𝐵 , 𝐷 } ∈ V
46 eleq2 ⊢ ( 𝑒 = { 𝐵 , 𝐷 } → ( 𝐶 ∈ 𝑒 ↔ 𝐶 ∈ { 𝐵 , 𝐷 } ) )
47 46 rexsng ⊢ ( { 𝐵 , 𝐷 } ∈ V → ( ∃ 𝑒 ∈ { { 𝐵 , 𝐷 } } 𝐶 ∈ 𝑒 ↔ 𝐶 ∈ { 𝐵 , 𝐷 } ) )
48 45 47 mp1i ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( ∃ 𝑒 ∈ { { 𝐵 , 𝐷 } } 𝐶 ∈ 𝑒 ↔ 𝐶 ∈ { 𝐵 , 𝐷 } ) )
49 elprg ⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ { 𝐵 , 𝐷 } ↔ ( 𝐶 = 𝐵 ∨ 𝐶 = 𝐷 ) ) )
50 4 49 syl ⊢ ( 𝜑 → ( 𝐶 ∈ { 𝐵 , 𝐷 } ↔ ( 𝐶 = 𝐵 ∨ 𝐶 = 𝐷 ) ) )
51 50 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( 𝐶 ∈ { 𝐵 , 𝐷 } ↔ ( 𝐶 = 𝐵 ∨ 𝐶 = 𝐷 ) ) )
52 44 48 51 3bitrd ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝐶 ∈ 𝑒 ↔ ( 𝐶 = 𝐵 ∨ 𝐶 = 𝐷 ) ) )
53 36 52 mtbird ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝐶 ∈ 𝑒 )
54 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
55 2 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → 𝐴 ∈ 𝑋 )
56 3 1 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
57 56 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
58 6 1 eleqtrrd ⊢ ( 𝜑 → 𝐷 ∈ ( Vtx ‘ 𝐺 ) )
59 58 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → 𝐷 ∈ ( Vtx ‘ 𝐺 ) )
60 8 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } )
61 simpl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → 𝐵 ≠ 𝐷 )
62 54 55 57 59 60 61 usgr1e ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → 𝐺 ∈ USGraph )
63 4 1 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
64 63 adantl ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
65 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
66 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
67 54 65 66 vtxdusgr0edgnel ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 ↔ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝐶 ∈ 𝑒 ) )
68 62 64 67 syl2anc ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 ↔ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) 𝐶 ∈ 𝑒 ) )
69 53 68 mpbird ⊢ ( ( 𝐵 ≠ 𝐷 ∧ 𝜑 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 )
70 69 ex ⊢ ( 𝐵 ≠ 𝐷 → ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 ) )
71 27 70 pm2.61ine ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 )