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