Metamath Proof Explorer

Theorem iswwlksnon

Description: The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis iswwlksnon.v ⊢ V = Vtx ⁡ G
Assertion iswwlksnon ⊢ A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B

Proof

Step Hyp Ref Expression
1 iswwlksnon.v ⊢ V = Vtx ⁡ G
2 0ov ⊢ A ∅ B = ∅
3 df-wwlksnon ⊢ WWalksNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b
4 3 mpondm0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N WWalksNOn G = ∅
5 4 oveqd ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WWalksNOn G B = A ∅ B
6 df-wwlksn ⊢ WWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1
7 6 mpondm0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N WWalksN G = ∅
8 7 rabeqdv ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B = w ∈ ∅ | w ⁡ 0 = A ∧ w ⁡ N = B
9 rab0 ⊢ w ∈ ∅ | w ⁡ 0 = A ∧ w ⁡ N = B = ∅
10 8 9 eqtrdi ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B = ∅
11 2 5 10 3eqtr4a ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
12 1 wwlksnon ⊢ N ∈ ℕ 0 ∧ G ∈ V → N WWalksNOn G = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
13 12 adantr ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → N WWalksNOn G = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
14 13 oveqd ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = A a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b B
15 eqid ⊢ a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
16 15 mpondm0 ⊢ ¬ A ∈ V ∧ B ∈ V → A a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b B = ∅
17 16 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → A a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b B = ∅
18 14 17 eqtrd ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = ∅
19 18 ex ⊢ N ∈ ℕ 0 ∧ G ∈ V → ¬ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = ∅
20 5 2 eqtrdi ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WWalksNOn G B = ∅
21 20 a1d ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → ¬ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = ∅
22 19 21 pm2.61i ⊢ ¬ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = ∅
23 1 wwlknllvtx ⊢ w ∈ N WWalksN G → w ⁡ 0 ∈ V ∧ w ⁡ N ∈ V
24 eleq1 ⊢ A = w ⁡ 0 → A ∈ V ↔ w ⁡ 0 ∈ V
25 24 eqcoms ⊢ w ⁡ 0 = A → A ∈ V ↔ w ⁡ 0 ∈ V
26 eleq1 ⊢ B = w ⁡ N → B ∈ V ↔ w ⁡ N ∈ V
27 26 eqcoms ⊢ w ⁡ N = B → B ∈ V ↔ w ⁡ N ∈ V
28 25 27 bi2anan9 ⊢ w ⁡ 0 = A ∧ w ⁡ N = B → A ∈ V ∧ B ∈ V ↔ w ⁡ 0 ∈ V ∧ w ⁡ N ∈ V
29 23 28 syl5ibrcom ⊢ w ∈ N WWalksN G → w ⁡ 0 = A ∧ w ⁡ N = B → A ∈ V ∧ B ∈ V
30 29 con3rr3 ⊢ ¬ A ∈ V ∧ B ∈ V → w ∈ N WWalksN G → ¬ w ⁡ 0 = A ∧ w ⁡ N = B
31 30 ralrimiv ⊢ ¬ A ∈ V ∧ B ∈ V → ∀ w ∈ N WWalksN G ¬ w ⁡ 0 = A ∧ w ⁡ N = B
32 rabeq0 ⊢ w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B = ∅ ↔ ∀ w ∈ N WWalksN G ¬ w ⁡ 0 = A ∧ w ⁡ N = B
33 31 32 sylibr ⊢ ¬ A ∈ V ∧ B ∈ V → w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B = ∅
34 22 33 eqtr4d ⊢ ¬ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
35 12 adantr ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → N WWalksNOn G = a ∈ V , b ∈ V ⟼ w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b
36 eqeq2 ⊢ a = A → w ⁡ 0 = a ↔ w ⁡ 0 = A
37 eqeq2 ⊢ b = B → w ⁡ N = b ↔ w ⁡ N = B
38 36 37 bi2anan9 ⊢ a = A ∧ b = B → w ⁡ 0 = a ∧ w ⁡ N = b ↔ w ⁡ 0 = A ∧ w ⁡ N = B
39 38 rabbidv ⊢ a = A ∧ b = B → w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
40 39 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ a = A ∧ b = B → w ∈ N WWalksN G | w ⁡ 0 = a ∧ w ⁡ N = b = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
41 simprl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → A ∈ V
42 simprr ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → B ∈ V
43 ovex ⊢ N WWalksN G ∈ V
44 43 rabex ⊢ w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B ∈ V
45 44 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B ∈ V
46 35 40 41 42 45 ovmpod ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B
47 11 34 46 ecase ⊢ A N WWalksNOn G B = w ∈ N WWalksN G | w ⁡ 0 = A ∧ w ⁡ N = B