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 19 23 raleqtrrdv 
 |-  ( ph -> A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) )
25 ralnex 
 |-  ( A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) )
26 24 25 sylib 
 |-  ( ph -> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) )
27 2 eleq2d 
 |-  ( ph -> ( D e. ( Vtx ` G ) <-> D e. V ) )
28 4 27 mpbird 
 |-  ( ph -> D e. ( Vtx ` G ) )
29 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
30 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
31 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
32 29 30 31 vtxd0nedgb 
 |-  ( D e. ( Vtx ` G ) -> ( ( ( VtxDeg ` G ) ` D ) = 0 <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) )
33 28 32 syl 
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` D ) = 0 <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) )
34 26 33 mpbird 
 |-  ( ph -> ( ( VtxDeg ` G ) ` D ) = 0 )