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 ∈ ℕ