Metamath Proof Explorer

Theorem wlkl0

Description: There is exactly one walk of length 0 on each vertex X . (Contributed by AV, 4-Jun-2022)

Ref Expression
Hypothesis clwlknon2num.v 
|- V = ( Vtx ` G )
Assertion wlkl0 
|- ( X e. V -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { <. (/) , { <. 0 , X >. } >. } )

Proof

Step Hyp Ref Expression
1 clwlknon2num.v 
 |-  V = ( Vtx ` G )
2 clwlkwlk 
 |-  ( w e. ( ClWalks ` G ) -> w e. ( Walks ` G ) )
3 wlkop 
 |-  ( w e. ( Walks ` G ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
4 2 3 syl 
 |-  ( w e. ( ClWalks ` G ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. )
5 fvex 
 |-  ( 1st ` w ) e. _V
6 hasheq0 
 |-  ( ( 1st ` w ) e. _V -> ( ( # ` ( 1st ` w ) ) = 0 <-> ( 1st ` w ) = (/) ) )
7 5 6 ax-mp 
 |-  ( ( # ` ( 1st ` w ) ) = 0 <-> ( 1st ` w ) = (/) )
8 7 biimpi 
 |-  ( ( # ` ( 1st ` w ) ) = 0 -> ( 1st ` w ) = (/) )
9 8 adantr 
 |-  ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> ( 1st ` w ) = (/) )
10 9 3ad2ant3 
 |-  ( ( X e. V /\ ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( 1st ` w ) = (/) )
11 9 adantl 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( 1st ` w ) = (/) )
12 11 breq1d 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) <-> (/) ( ClWalks ` G ) ( 2nd ` w ) ) )
13 1 1vgrex 
 |-  ( X e. V -> G e. _V )
14 1 0clwlk 
 |-  ( G e. _V -> ( (/) ( ClWalks ` G ) ( 2nd ` w ) <-> ( 2nd ` w ) : ( 0 ... 0 ) --> V ) )
15 13 14 syl 
 |-  ( X e. V -> ( (/) ( ClWalks ` G ) ( 2nd ` w ) <-> ( 2nd ` w ) : ( 0 ... 0 ) --> V ) )
16 15 adantr 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( (/) ( ClWalks ` G ) ( 2nd ` w ) <-> ( 2nd ` w ) : ( 0 ... 0 ) --> V ) )
17 12 16 bitrd 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) <-> ( 2nd ` w ) : ( 0 ... 0 ) --> V ) )
18 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
19 18 feq2i 
 |-  ( ( 2nd ` w ) : ( 0 ... 0 ) --> V <-> ( 2nd ` w ) : { 0 } --> V )
20 c0ex 
 |-  0 e. _V
21 20 fsn2 
 |-  ( ( 2nd ` w ) : { 0 } --> V <-> ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) )
22 simprr 
 |-  ( ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) /\ ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) ) -> ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } )
23 simprr 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( 2nd ` w ) ` 0 ) = X )
24 23 adantr 
 |-  ( ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) /\ ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) ) -> ( ( 2nd ` w ) ` 0 ) = X )
25 24 opeq2d 
 |-  ( ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) /\ ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) ) -> <. 0 , ( ( 2nd ` w ) ` 0 ) >. = <. 0 , X >. )
26 25 sneqd 
 |-  ( ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) /\ ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) ) -> { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } = { <. 0 , X >. } )
27 22 26 eqtrd 
 |-  ( ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) /\ ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) ) -> ( 2nd ` w ) = { <. 0 , X >. } )
28 27 ex 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( ( ( 2nd ` w ) ` 0 ) e. V /\ ( 2nd ` w ) = { <. 0 , ( ( 2nd ` w ) ` 0 ) >. } ) -> ( 2nd ` w ) = { <. 0 , X >. } ) )
29 21 28 biimtrid 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( 2nd ` w ) : { 0 } --> V -> ( 2nd ` w ) = { <. 0 , X >. } ) )
30 19 29 biimtrid 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( 2nd ` w ) : ( 0 ... 0 ) --> V -> ( 2nd ` w ) = { <. 0 , X >. } ) )
31 17 30 sylbid 
 |-  ( ( X e. V /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) -> ( 2nd ` w ) = { <. 0 , X >. } ) )
32 31 ex 
 |-  ( X e. V -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) -> ( 2nd ` w ) = { <. 0 , X >. } ) ) )
33 32 com23 
 |-  ( X e. V -> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> ( 2nd ` w ) = { <. 0 , X >. } ) ) )
34 33 3imp 
 |-  ( ( X e. V /\ ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> ( 2nd ` w ) = { <. 0 , X >. } )
35 10 34 opeq12d 
 |-  ( ( X e. V /\ ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> <. ( 1st ` w ) , ( 2nd ` w ) >. = <. (/) , { <. 0 , X >. } >. )
36 35 3exp 
 |-  ( X e. V -> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> <. ( 1st ` w ) , ( 2nd ` w ) >. = <. (/) , { <. 0 , X >. } >. ) ) )
37 eleq1 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( w e. ( ClWalks ` G ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ClWalks ` G ) ) )
38 df-br 
 |-  ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) <-> <. ( 1st ` w ) , ( 2nd ` w ) >. e. ( ClWalks ` G ) )
39 37 38 bitr4di 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( w e. ( ClWalks ` G ) <-> ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) ) )
40 eqeq1 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( w = <. (/) , { <. 0 , X >. } >. <-> <. ( 1st ` w ) , ( 2nd ` w ) >. = <. (/) , { <. 0 , X >. } >. ) )
41 40 imbi2d 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> w = <. (/) , { <. 0 , X >. } >. ) <-> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> <. ( 1st ` w ) , ( 2nd ` w ) >. = <. (/) , { <. 0 , X >. } >. ) ) )
42 39 41 imbi12d 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( ( w e. ( ClWalks ` G ) -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> w = <. (/) , { <. 0 , X >. } >. ) ) <-> ( ( 1st ` w ) ( ClWalks ` G ) ( 2nd ` w ) -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> <. ( 1st ` w ) , ( 2nd ` w ) >. = <. (/) , { <. 0 , X >. } >. ) ) ) )
43 36 42 imbitrrid 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( X e. V -> ( w e. ( ClWalks ` G ) -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> w = <. (/) , { <. 0 , X >. } >. ) ) ) )
44 43 com23 
 |-  ( w = <. ( 1st ` w ) , ( 2nd ` w ) >. -> ( w e. ( ClWalks ` G ) -> ( X e. V -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> w = <. (/) , { <. 0 , X >. } >. ) ) ) )
45 4 44 mpcom 
 |-  ( w e. ( ClWalks ` G ) -> ( X e. V -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> w = <. (/) , { <. 0 , X >. } >. ) ) )
46 45 com12 
 |-  ( X e. V -> ( w e. ( ClWalks ` G ) -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) -> w = <. (/) , { <. 0 , X >. } >. ) ) )
47 46 impd 
 |-  ( X e. V -> ( ( w e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) -> w = <. (/) , { <. 0 , X >. } >. ) )
48 eqidd 
 |-  ( X e. V -> (/) = (/) )
49 20 a1i 
 |-  ( X e. V -> 0 e. _V )
50 snidg 
 |-  ( X e. V -> X e. { X } )
51 49 50 fsnd 
 |-  ( X e. V -> { <. 0 , X >. } : { 0 } --> { X } )
52 1 0clwlkv 
 |-  ( ( X e. V /\ (/) = (/) /\ { <. 0 , X >. } : { 0 } --> { X } ) -> (/) ( ClWalks ` G ) { <. 0 , X >. } )
53 48 51 52 mpd3an23 
 |-  ( X e. V -> (/) ( ClWalks ` G ) { <. 0 , X >. } )
54 hash0 
 |-  ( # ` (/) ) = 0
55 54 a1i 
 |-  ( X e. V -> ( # ` (/) ) = 0 )
56 fvsng 
 |-  ( ( 0 e. _V /\ X e. V ) -> ( { <. 0 , X >. } ` 0 ) = X )
57 20 56 mpan 
 |-  ( X e. V -> ( { <. 0 , X >. } ` 0 ) = X )
58 53 55 57 jca32 
 |-  ( X e. V -> ( (/) ( ClWalks ` G ) { <. 0 , X >. } /\ ( ( # ` (/) ) = 0 /\ ( { <. 0 , X >. } ` 0 ) = X ) ) )
59 eleq1 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( w e. ( ClWalks ` G ) <-> <. (/) , { <. 0 , X >. } >. e. ( ClWalks ` G ) ) )
60 df-br 
 |-  ( (/) ( ClWalks ` G ) { <. 0 , X >. } <-> <. (/) , { <. 0 , X >. } >. e. ( ClWalks ` G ) )
61 59 60 bitr4di 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( w e. ( ClWalks ` G ) <-> (/) ( ClWalks ` G ) { <. 0 , X >. } ) )
62 0ex 
 |-  (/) e. _V
63 snex 
 |-  { <. 0 , X >. } e. _V
64 62 63 op1std 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( 1st ` w ) = (/) )
65 64 fveqeq2d 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( ( # ` ( 1st ` w ) ) = 0 <-> ( # ` (/) ) = 0 ) )
66 62 63 op2ndd 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( 2nd ` w ) = { <. 0 , X >. } )
67 66 fveq1d 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( ( 2nd ` w ) ` 0 ) = ( { <. 0 , X >. } ` 0 ) )
68 67 eqeq1d 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( ( ( 2nd ` w ) ` 0 ) = X <-> ( { <. 0 , X >. } ` 0 ) = X ) )
69 65 68 anbi12d 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) <-> ( ( # ` (/) ) = 0 /\ ( { <. 0 , X >. } ` 0 ) = X ) ) )
70 61 69 anbi12d 
 |-  ( w = <. (/) , { <. 0 , X >. } >. -> ( ( w e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) <-> ( (/) ( ClWalks ` G ) { <. 0 , X >. } /\ ( ( # ` (/) ) = 0 /\ ( { <. 0 , X >. } ` 0 ) = X ) ) ) )
71 58 70 syl5ibrcom 
 |-  ( X e. V -> ( w = <. (/) , { <. 0 , X >. } >. -> ( w e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) ) )
72 47 71 impbid 
 |-  ( X e. V -> ( ( w e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) <-> w = <. (/) , { <. 0 , X >. } >. ) )
73 72 alrimiv 
 |-  ( X e. V -> A. w ( ( w e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) <-> w = <. (/) , { <. 0 , X >. } >. ) )
74 rabeqsn 
 |-  ( { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { <. (/) , { <. 0 , X >. } >. } <-> A. w ( ( w e. ( ClWalks ` G ) /\ ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) ) <-> w = <. (/) , { <. 0 , X >. } >. ) )
75 73 74 sylibr 
 |-  ( X e. V -> { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = 0 /\ ( ( 2nd ` w ) ` 0 ) = X ) } = { <. (/) , { <. 0 , X >. } >. } )