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≤1st⁡w
clwlkclwwlkf.a ⊢A=1st⁡U
clwlkclwwlkf.b ⊢B=2nd⁡U
Assertion clwlkclwwlkflem ⊢U∈C→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢C=w∈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∈C↔U∈ClWalks⁡G∧1≤A
9 clwlkwlk ⊢U∈ClWalks⁡G→U∈Walks⁡G
10 wlkop ⊢U∈Walks⁡G→U=1st⁡U2nd⁡U
11 2 3 opeq12i ⊢AB=1st⁡U2nd⁡U
12 11 eqeq2i ⊢U=AB↔U=1st⁡U2nd⁡U
13 eleq1 ⊢U=AB→U∈ClWalks⁡G↔AB∈ClWalks⁡G
14 df-br ⊢AClWalks⁡GB↔AB∈ClWalks⁡G
15 isclwlk ⊢AClWalks⁡GB↔AWalks⁡GB∧B⁡0=B⁡A
16 wlkcl ⊢AWalks⁡GB→A∈ℕ0
17 elnnnn0c ⊢A∈ℕ↔A∈ℕ0∧1≤A
18 17 a1i ⊢AWalks⁡GB→A∈ℕ↔A∈ℕ0∧1≤A
19 16 18 mpbirand ⊢AWalks⁡GB→A∈ℕ↔1≤A
20 19 bicomd ⊢AWalks⁡GB→1≤A↔A∈ℕ
21 20 adantr ⊢AWalks⁡GB∧B⁡0=B⁡A→1≤A↔A∈ℕ
22 21 pm5.32i ⊢AWalks⁡GB∧B⁡0=B⁡A∧1≤A↔AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
23 df-3an ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ↔AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
24 22 23 sylbb2 ⊢AWalks⁡GB∧B⁡0=B⁡A∧1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
25 24 ex ⊢AWalks⁡GB∧B⁡0=B⁡A→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
26 15 25 sylbi ⊢AClWalks⁡GB→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
27 14 26 sylbir ⊢AB∈ClWalks⁡G→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
28 13 27 syl6bi ⊢U=AB→U∈ClWalks⁡G→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
29 12 28 sylbir ⊢U=1st⁡U2nd⁡U→U∈ClWalks⁡G→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
30 10 29 syl ⊢U∈Walks⁡G→U∈ClWalks⁡G→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
31 9 30 mpcom ⊢U∈ClWalks⁡G→1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
32 31 imp ⊢U∈ClWalks⁡G∧1≤A→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
33 8 32 sylbi ⊢U∈C→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ