Metamath Proof Explorer

Theorem clwlkclwwlkflem

Description: Lemma for clwlkclwwlkf . (Contributed by AV, 24-May-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c 
|- C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
clwlkclwwlkf.a 
|- A = ( 1st ` U )
clwlkclwwlkf.b 
|- B = ( 2nd ` U )
Assertion clwlkclwwlkflem 
|- ( U e. C -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c 
 |-  C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
2 clwlkclwwlkf.a 
 |-  A = ( 1st ` U )
3 clwlkclwwlkf.b 
 |-  B = ( 2nd ` U )
4 fveq2 
 |-  ( w = U -> ( 1st ` w ) = ( 1st ` U ) )
5 4 2 eqtr4di 
 |-  ( w = U -> ( 1st ` w ) = A )
6 5 fveq2d 
 |-  ( w = U -> ( # ` ( 1st ` w ) ) = ( # ` A ) )
7 6 breq2d 
 |-  ( w = U -> ( 1 <_ ( # ` ( 1st ` w ) ) <-> 1 <_ ( # ` A ) ) )
8 7 1 elrab2 
 |-  ( U e. C <-> ( U e. ( ClWalks ` G ) /\ 1 <_ ( # ` A ) ) )
9 clwlkwlk 
 |-  ( U e. ( ClWalks ` G ) -> U e. ( Walks ` G ) )
10 wlkop 
 |-  ( U e. ( Walks ` G ) -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
11 2 3 opeq12i 
 |-  <. A , B >. = <. ( 1st ` U ) , ( 2nd ` U ) >.
12 11 eqeq2i 
 |-  ( U = <. A , B >. <-> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
13 eleq1 
 |-  ( U = <. A , B >. -> ( U e. ( ClWalks ` G ) <-> <. A , B >. e. ( ClWalks ` G ) ) )
14 df-br 
 |-  ( A ( ClWalks ` G ) B <-> <. A , B >. e. ( ClWalks ` G ) )
15 isclwlk 
 |-  ( A ( ClWalks ` G ) B <-> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) )
16 wlkcl 
 |-  ( A ( Walks ` G ) B -> ( # ` A ) e. NN0 )
17 elnnnn0c 
 |-  ( ( # ` A ) e. NN <-> ( ( # ` A ) e. NN0 /\ 1 <_ ( # ` A ) ) )
18 17 a1i 
 |-  ( A ( Walks ` G ) B -> ( ( # ` A ) e. NN <-> ( ( # ` A ) e. NN0 /\ 1 <_ ( # ` A ) ) ) )
19 16 18 mpbirand 
 |-  ( A ( Walks ` G ) B -> ( ( # ` A ) e. NN <-> 1 <_ ( # ` A ) ) )
20 19 bicomd 
 |-  ( A ( Walks ` G ) B -> ( 1 <_ ( # ` A ) <-> ( # ` A ) e. NN ) )
21 20 adantr 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) -> ( 1 <_ ( # ` A ) <-> ( # ` A ) e. NN ) )
22 21 pm5.32i 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) /\ 1 <_ ( # ` A ) ) <-> ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) /\ ( # ` A ) e. NN ) )
23 df-3an 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) <-> ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) /\ ( # ` A ) e. NN ) )
24 22 23 sylbb2 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) /\ 1 <_ ( # ` A ) ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) )
25 24 ex 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) ) -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) )
26 15 25 sylbi 
 |-  ( A ( ClWalks ` G ) B -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) )
27 14 26 sylbir 
 |-  ( <. A , B >. e. ( ClWalks ` G ) -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) )
28 13 27 syl6bi 
 |-  ( U = <. A , B >. -> ( U e. ( ClWalks ` G ) -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) ) )
29 12 28 sylbir 
 |-  ( U = <. ( 1st ` U ) , ( 2nd ` U ) >. -> ( U e. ( ClWalks ` G ) -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) ) )
30 10 29 syl 
 |-  ( U e. ( Walks ` G ) -> ( U e. ( ClWalks ` G ) -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) ) )
31 9 30 mpcom 
 |-  ( U e. ( ClWalks ` G ) -> ( 1 <_ ( # ` A ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) ) )
32 31 imp 
 |-  ( ( U e. ( ClWalks ` G ) /\ 1 <_ ( # ` A ) ) -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) )
33 8 32 sylbi 
 |-  ( U e. C -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) )