Metamath Proof Explorer


Theorem clwlkclwwlkflem

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

Ref Expression
Hypotheses clwlkclwwlkf.c C = w ClWalks G | 1 1 st w
clwlkclwwlkf.a A = 1 st U
clwlkclwwlkf.b B = 2 nd U
Assertion clwlkclwwlkflem U C A Walks G B B 0 = B A A

Proof

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