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
|- ( ph -> ( iEdg ` G ) = { <. A , E >. } )
1hevtxdg0.v
|- ( ph -> ( Vtx ` G ) = V )
1hevtxdg0.a
|- ( ph -> A e. X )
1hevtxdg0.d
|- ( ph -> D e. V )
1hevtxdg0.e
|- ( ph -> E e. Y )
1hevtxdg0.n
|- ( ph -> D e/ E )
Assertion 1hevtxdg0
|- ( ph -> ( ( VtxDeg ` G ) ` D ) = 0 )

Proof

Step Hyp Ref Expression
1 1hevtxdg0.i
 |-  ( ph -> ( iEdg ` G ) = { <. A , E >. } )
2 1hevtxdg0.v
 |-  ( ph -> ( Vtx ` G ) = V )
3 1hevtxdg0.a
 |-  ( ph -> A e. X )
4 1hevtxdg0.d
 |-  ( ph -> D e. V )
5 1hevtxdg0.e
 |-  ( ph -> E e. Y )
6 1hevtxdg0.n
 |-  ( ph -> D e/ E )
7 df-nel
 |-  ( D e/ E <-> -. D e. E )
8 6 7 sylib
 |-  ( ph -> -. D e. E )
9 1 fveq1d
 |-  ( ph -> ( ( iEdg ` G ) ` A ) = ( { <. A , E >. } ` A ) )
10 fvsng
 |-  ( ( A e. X /\ E e. Y ) -> ( { <. A , E >. } ` A ) = E )
11 3 5 10 syl2anc
 |-  ( ph -> ( { <. A , E >. } ` A ) = E )
12 9 11 eqtrd
 |-  ( ph -> ( ( iEdg ` G ) ` A ) = E )
13 8 12 neleqtrrd
 |-  ( ph -> -. D e. ( ( iEdg ` G ) ` A ) )
14 fveq2
 |-  ( x = A -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` A ) )
15 14 eleq2d
 |-  ( x = A -> ( D e. ( ( iEdg ` G ) ` x ) <-> D e. ( ( iEdg ` G ) ` A ) ) )
16 15 notbid
 |-  ( x = A -> ( -. D e. ( ( iEdg ` G ) ` x ) <-> -. D e. ( ( iEdg ` G ) ` A ) ) )
17 16 ralsng
 |-  ( A e. X -> ( A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) <-> -. D e. ( ( iEdg ` G ) ` A ) ) )
18 3 17 syl
 |-  ( ph -> ( A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) <-> -. D e. ( ( iEdg ` G ) ` A ) ) )
19 13 18 mpbird
 |-  ( ph -> A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) )
20 1 dmeqd
 |-  ( ph -> dom ( iEdg ` G ) = dom { <. A , E >. } )
21 dmsnopg
 |-  ( E e. Y -> dom { <. A , E >. } = { A } )
22 5 21 syl
 |-  ( ph -> dom { <. A , E >. } = { A } )
23 20 22 eqtrd
 |-  ( ph -> dom ( iEdg ` G ) = { A } )
24 23 raleqdv
 |-  ( ph -> ( A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) <-> A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) ) )
25 19 24 mpbird
 |-  ( ph -> A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) )
26 ralnex
 |-  ( A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) )
27 25 26 sylib
 |-  ( ph -> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) )
28 2 eleq2d
 |-  ( ph -> ( D e. ( Vtx ` G ) <-> D e. V ) )
29 4 28 mpbird
 |-  ( ph -> D e. ( Vtx ` G ) )
30 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
31 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
32 eqid
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
33 30 31 32 vtxd0nedgb
 |-  ( D e. ( Vtx ` G ) -> ( ( ( VtxDeg ` G ) ` D ) = 0 <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) )
34 29 33 syl
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` D ) = 0 <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) )
35 27 34 mpbird
 |-  ( ph -> ( ( VtxDeg ` G ) ` D ) = 0 )