Metamath Proof Explorer

Theorem 1hevtxdg1

Description: The vertex degree of vertex D in a graph G with only one hyperedge E (not being a loop) is 1 if D is incident with the edge E . (Contributed by AV, 2-Mar-2021) (Proof shortened by AV, 17-Apr-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 )
1hevtxdg1.e 
|- ( ph -> E e. ~P V )
1hevtxdg1.n 
|- ( ph -> D e. E )
1hevtxdg1.l 
|- ( ph -> 2 <_ ( # ` E ) )
Assertion 1hevtxdg1 
|- ( ph -> ( ( VtxDeg ` G ) ` D ) = 1 )

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 1hevtxdg1.e 
 |-  ( ph -> E e. ~P V )
6 1hevtxdg1.n 
 |-  ( ph -> D e. E )
7 1hevtxdg1.l 
 |-  ( ph -> 2 <_ ( # ` E ) )
8 1 dmeqd 
 |-  ( ph -> dom ( iEdg ` G ) = dom { <. A , E >. } )
9 dmsnopg 
 |-  ( E e. ~P V -> dom { <. A , E >. } = { A } )
10 5 9 syl 
 |-  ( ph -> dom { <. A , E >. } = { A } )
11 8 10 eqtrd 
 |-  ( ph -> dom ( iEdg ` G ) = { A } )
12 fveq2 
 |-  ( x = E -> ( # ` x ) = ( # ` E ) )
13 12 breq2d 
 |-  ( x = E -> ( 2 <_ ( # ` x ) <-> 2 <_ ( # ` E ) ) )
14 2 pweqd 
 |-  ( ph -> ~P ( Vtx ` G ) = ~P V )
15 5 14 eleqtrrd 
 |-  ( ph -> E e. ~P ( Vtx ` G ) )
16 13 15 7 elrabd 
 |-  ( ph -> E e. { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
17 3 16 fsnd 
 |-  ( ph -> { <. A , E >. } : { A } --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
18 17 adantr 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> { <. A , E >. } : { A } --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
19 1 adantr 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( iEdg ` G ) = { <. A , E >. } )
20 simpr 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> dom ( iEdg ` G ) = { A } )
21 19 20 feq12d 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } <-> { <. A , E >. } : { A } --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } ) )
22 18 21 mpbird 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } )
23 4 2 eleqtrrd 
 |-  ( ph -> D e. ( Vtx ` G ) )
24 23 adantr 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> D e. ( Vtx ` G ) )
25 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
26 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
27 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
28 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
29 25 26 27 28 vtxdlfgrval 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | 2 <_ ( # ` x ) } /\ D e. ( Vtx ` G ) ) -> ( ( VtxDeg ` G ) ` D ) = ( # ` { x e. dom ( iEdg ` G ) | D e. ( ( iEdg ` G ) ` x ) } ) )
30 22 24 29 syl2anc 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( ( VtxDeg ` G ) ` D ) = ( # ` { x e. dom ( iEdg ` G ) | D e. ( ( iEdg ` G ) ` x ) } ) )
31 rabeq 
 |-  ( dom ( iEdg ` G ) = { A } -> { x e. dom ( iEdg ` G ) | D e. ( ( iEdg ` G ) ` x ) } = { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } )
32 31 adantl 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> { x e. dom ( iEdg ` G ) | D e. ( ( iEdg ` G ) ` x ) } = { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } )
33 32 fveq2d 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( # ` { x e. dom ( iEdg ` G ) | D e. ( ( iEdg ` G ) ` x ) } ) = ( # ` { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } ) )
34 fveq2 
 |-  ( x = A -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` A ) )
35 34 eleq2d 
 |-  ( x = A -> ( D e. ( ( iEdg ` G ) ` x ) <-> D e. ( ( iEdg ` G ) ` A ) ) )
36 35 rabsnif 
 |-  { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } = if ( D e. ( ( iEdg ` G ) ` A ) , { A } , (/) )
37 1 fveq1d 
 |-  ( ph -> ( ( iEdg ` G ) ` A ) = ( { <. A , E >. } ` A ) )
38 fvsng 
 |-  ( ( A e. X /\ E e. ~P V ) -> ( { <. A , E >. } ` A ) = E )
39 3 5 38 syl2anc 
 |-  ( ph -> ( { <. A , E >. } ` A ) = E )
40 37 39 eqtrd 
 |-  ( ph -> ( ( iEdg ` G ) ` A ) = E )
41 6 40 eleqtrrd 
 |-  ( ph -> D e. ( ( iEdg ` G ) ` A ) )
42 41 iftrued 
 |-  ( ph -> if ( D e. ( ( iEdg ` G ) ` A ) , { A } , (/) ) = { A } )
43 36 42 syl5eq 
 |-  ( ph -> { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } = { A } )
44 43 fveq2d 
 |-  ( ph -> ( # ` { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } ) = ( # ` { A } ) )
45 hashsng 
 |-  ( A e. X -> ( # ` { A } ) = 1 )
46 3 45 syl 
 |-  ( ph -> ( # ` { A } ) = 1 )
47 44 46 eqtrd 
 |-  ( ph -> ( # ` { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } ) = 1 )
48 47 adantr 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( # ` { x e. { A } | D e. ( ( iEdg ` G ) ` x ) } ) = 1 )
49 30 33 48 3eqtrd 
 |-  ( ( ph /\ dom ( iEdg ` G ) = { A } ) -> ( ( VtxDeg ` G ) ` D ) = 1 )
50 11 49 mpdan 
 |-  ( ph -> ( ( VtxDeg ` G ) ` D ) = 1 )