Metamath Proof Explorer

Theorem clwlkclwwlkf1lem2

Description: Lemma 2 for clwlkclwwlkf1 . (Contributed by AV, 24-May-2022) (Revised by AV, 30-Oct-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
clwlkclwwlkf.d ⊢ D = 1 st ⁡ W
clwlkclwwlkf.e ⊢ E = 2 nd ⁡ W
Assertion clwlkclwwlkf1lem2 ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i

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 clwlkclwwlkf.d ⊢ D = 1 st ⁡ W
5 clwlkclwwlkf.e ⊢ E = 2 nd ⁡ W
6 1 2 3 clwlkclwwlkflem ⊢ U ∈ C → A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ
7 1 4 5 clwlkclwwlkflem ⊢ W ∈ C → D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ
8 6 7 anim12i ⊢ U ∈ C ∧ W ∈ C → A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 9 wlkpwrd ⊢ A Walks ⁡ G B → B ∈ Word Vtx ⁡ G
11 10 3ad2ant1 ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → B ∈ Word Vtx ⁡ G
12 9 wlkpwrd ⊢ D Walks ⁡ G E → E ∈ Word Vtx ⁡ G
13 12 3ad2ant1 ⊢ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → E ∈ Word Vtx ⁡ G
14 11 13 anim12i ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → B ∈ Word Vtx ⁡ G ∧ E ∈ Word Vtx ⁡ G
15 nnnn0 ⊢ A ∈ ℕ → A ∈ ℕ 0
16 15 3ad2ant3 ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → A ∈ ℕ 0
17 nnnn0 ⊢ D ∈ ℕ → D ∈ ℕ 0
18 17 3ad2ant3 ⊢ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → D ∈ ℕ 0
19 16 18 anim12i ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → A ∈ ℕ 0 ∧ D ∈ ℕ 0
20 wlklenvp1 ⊢ A Walks ⁡ G B → B = A + 1
21 nnre ⊢ A ∈ ℕ → A ∈ ℝ
22 21 lep1d ⊢ A ∈ ℕ → A ≤ A + 1
23 breq2 ⊢ B = A + 1 → A ≤ B ↔ A ≤ A + 1
24 22 23 syl5ibr ⊢ B = A + 1 → A ∈ ℕ → A ≤ B
25 20 24 syl ⊢ A Walks ⁡ G B → A ∈ ℕ → A ≤ B
26 25 a1d ⊢ A Walks ⁡ G B → B ⁡ 0 = B ⁡ A → A ∈ ℕ → A ≤ B
27 26 3imp ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → A ≤ B
28 wlklenvp1 ⊢ D Walks ⁡ G E → E = D + 1
29 nnre ⊢ D ∈ ℕ → D ∈ ℝ
30 29 lep1d ⊢ D ∈ ℕ → D ≤ D + 1
31 breq2 ⊢ E = D + 1 → D ≤ E ↔ D ≤ D + 1
32 30 31 syl5ibr ⊢ E = D + 1 → D ∈ ℕ → D ≤ E
33 28 32 syl ⊢ D Walks ⁡ G E → D ∈ ℕ → D ≤ E
34 33 a1d ⊢ D Walks ⁡ G E → E ⁡ 0 = E ⁡ D → D ∈ ℕ → D ≤ E
35 34 3imp ⊢ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → D ≤ E
36 27 35 anim12i ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → A ≤ B ∧ D ≤ E
37 14 19 36 3jca ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → B ∈ Word Vtx ⁡ G ∧ E ∈ Word Vtx ⁡ G ∧ A ∈ ℕ 0 ∧ D ∈ ℕ 0 ∧ A ≤ B ∧ D ≤ E
38 pfxeq ⊢ B ∈ Word Vtx ⁡ G ∧ E ∈ Word Vtx ⁡ G ∧ A ∈ ℕ 0 ∧ D ∈ ℕ 0 ∧ A ≤ B ∧ D ≤ E → B prefix A = E prefix D ↔ A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i
39 8 37 38 3syl ⊢ U ∈ C ∧ W ∈ C → B prefix A = E prefix D ↔ A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i
40 39 biimp3a ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i