Metamath Proof Explorer

Theorem 1egrvtxdg1

Description: The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's 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 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
1egrvtxdg1.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
Assertion 1egrvtxdg1 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )

Proof

Step Hyp Ref Expression
1 1egrvtxdg1.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2 1egrvtxdg1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 1egrvtxdg1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4 1egrvtxdg1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 1egrvtxdg1.n ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
6 1egrvtxdg1.i ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 3 1 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
9 4 1 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
10 7 2 8 9 6 5 usgr1e ⊢ ( 𝜑 → 𝐺 ∈ USGraph )
11 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
12 eqid ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
13 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
14 7 11 12 13 vtxdusgrval ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
15 10 8 14 syl2anc ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
16 dmeq ⊢ ( ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
17 16 adantl ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } )
18 prex ⊢ { 𝐵 , 𝐶 } ∈ V
19 dmsnopg ⊢ ( { 𝐵 , 𝐶 } ∈ V → dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { 𝐴 } )
20 18 19 mp1i ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → dom { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } = { 𝐴 } )
21 17 20 eqtrd ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
22 fveq1 ⊢ ( ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) )
23 22 eleq2d ⊢ ( ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } → ( 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) ) )
25 21 24 rabeqbidv ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } )
26 25 fveq2d ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) )
27 fveq2 ⊢ ( 𝑥 = 𝐴 → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) )
28 27 eleq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) ↔ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) ) )
29 28 rabsnif ⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } = if ( 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) , { 𝐴 } , ∅ )
30 prid1g ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 , 𝐶 } )
31 3 30 syl ⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 , 𝐶 } )
32 fvsng ⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝐵 , 𝐶 } ∈ V ) → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) = { 𝐵 , 𝐶 } )
33 2 18 32 sylancl ⊢ ( 𝜑 → ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) = { 𝐵 , 𝐶 } )
34 31 33 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) )
35 34 iftrued ⊢ ( 𝜑 → if ( 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝐴 ) , { 𝐴 } , ∅ ) = { 𝐴 } )
36 29 35 syl5eq ⊢ ( 𝜑 → { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } = { 𝐴 } )
37 36 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝐴 } ) )
38 hashsng ⊢ ( 𝐴 ∈ 𝑋 → ( ♯ ‘ { 𝐴 } ) = 1 )
39 2 38 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 } ) = 1 )
40 37 39 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) = 1 )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝐵 ∈ ( { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ‘ 𝑥 ) } ) = 1 )
42 26 41 eqtrd ⊢ ( ( 𝜑 ∧ ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐶 } ⟩ } ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 )
43 6 42 mpdan ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝐵 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 )
44 15 43 eqtrd ⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐵 ) = 1 )