Metamath Proof Explorer


Theorem 1hevtxdg0

Description: The vertex degree of vertex D in a graph G with only one hyperedge E is 0 if D is not incident with the edge E . (Contributed by AV, 2-Mar-2021)

Ref Expression
Hypotheses 1hevtxdg0.i ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
1hevtxdg0.v ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
1hevtxdg0.a ( 𝜑𝐴𝑋 )
1hevtxdg0.d ( 𝜑𝐷𝑉 )
1hevtxdg0.e ( 𝜑𝐸𝑌 )
1hevtxdg0.n ( 𝜑𝐷𝐸 )
Assertion 1hevtxdg0 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 )

Proof

Step Hyp Ref Expression
1 1hevtxdg0.i ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , 𝐸 ⟩ } )
2 1hevtxdg0.v ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3 1hevtxdg0.a ( 𝜑𝐴𝑋 )
4 1hevtxdg0.d ( 𝜑𝐷𝑉 )
5 1hevtxdg0.e ( 𝜑𝐸𝑌 )
6 1hevtxdg0.n ( 𝜑𝐷𝐸 )
7 df-nel ( 𝐷𝐸 ↔ ¬ 𝐷𝐸 )
8 6 7 sylib ( 𝜑 → ¬ 𝐷𝐸 )
9 1 fveq1d ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) )
10 fvsng ( ( 𝐴𝑋𝐸𝑌 ) → ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐸 )
11 3 5 10 syl2anc ( 𝜑 → ( { ⟨ 𝐴 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐸 )
12 9 11 eqtrd ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = 𝐸 )
13 8 12 neleqtrrd ( 𝜑 → ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) )
14 fveq2 ( 𝑥 = 𝐴 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) )
15 14 eleq2d ( 𝑥 = 𝐴 → ( 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
16 15 notbid ( 𝑥 = 𝐴 → ( ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
17 16 ralsng ( 𝐴𝑋 → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
18 3 17 syl ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) )
19 13 18 mpbird ( 𝜑 → ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
20 1 dmeqd ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , 𝐸 ⟩ } )
21 dmsnopg ( 𝐸𝑌 → dom { ⟨ 𝐴 , 𝐸 ⟩ } = { 𝐴 } )
22 5 21 syl ( 𝜑 → dom { ⟨ 𝐴 , 𝐸 ⟩ } = { 𝐴 } )
23 20 22 eqtrd ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
24 23 raleqdv ( 𝜑 → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
25 19 24 mpbird ( 𝜑 → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
26 ralnex ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
27 25 26 sylib ( 𝜑 → ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
28 2 eleq2d ( 𝜑 → ( 𝐷 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐷𝑉 ) )
29 4 28 mpbird ( 𝜑𝐷 ∈ ( Vtx ‘ 𝐺 ) )
30 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
31 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
32 eqid ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
33 30 31 32 vtxd0nedgb ( 𝐷 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
34 29 33 syl ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
35 27 34 mpbird ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 )