Metamath Proof Explorer

Theorem iswspthsnon

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

Ref Expression
Hypothesis iswspthsnon.v ⊢ V = Vtx ⁡ G
Assertion iswspthsnon ⊢ A N WSPathsNOn G B = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w

Proof

Step Hyp Ref Expression
1 iswspthsnon.v ⊢ V = Vtx ⁡ G
2 0ov ⊢ A ∅ B = ∅
3 df-wspthsnon ⊢ WSPathsNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
4 3 mpondm0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → N WSPathsNOn G = ∅
5 4 oveqd ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WSPathsNOn G B = A ∅ B
6 id ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → ¬ N ∈ ℕ 0 ∧ G ∈ V
7 6 intnanrd ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → ¬ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V
8 1 wwlksnon0 ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → A N WWalksNOn G B = ∅
9 7 8 syl ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WWalksNOn G B = ∅
10 9 rabeqdv ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w = w ∈ ∅ | ∃ f f A SPathsOn ⁡ G B w
11 rab0 ⊢ w ∈ ∅ | ∃ f f A SPathsOn ⁡ G B w = ∅
12 10 11 eqtrdi ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w = ∅
13 2 5 12 3eqtr4a ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WSPathsNOn G B = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w
14 1 wspthsnon ⊢ N ∈ ℕ 0 ∧ G ∈ V → N WSPathsNOn G = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
15 14 adantr ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → N WSPathsNOn G = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
16 15 oveqd ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = A a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w B
17 eqid ⊢ a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
18 17 mpondm0 ⊢ ¬ A ∈ V ∧ B ∈ V → A a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w B = ∅
19 18 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → A a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w B = ∅
20 16 19 eqtrd ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ ¬ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = ∅
21 20 ex ⊢ N ∈ ℕ 0 ∧ G ∈ V → ¬ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = ∅
22 5 2 eqtrdi ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → A N WSPathsNOn G B = ∅
23 22 a1d ⊢ ¬ N ∈ ℕ 0 ∧ G ∈ V → ¬ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = ∅
24 21 23 pm2.61i ⊢ ¬ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = ∅
25 1 wwlksonvtx ⊢ w ∈ A N WWalksNOn G B → A ∈ V ∧ B ∈ V
26 25 pm2.24d ⊢ w ∈ A N WWalksNOn G B → ¬ A ∈ V ∧ B ∈ V → ¬ f A SPathsOn ⁡ G B w
27 26 impcom ⊢ ¬ A ∈ V ∧ B ∈ V ∧ w ∈ A N WWalksNOn G B → ¬ f A SPathsOn ⁡ G B w
28 27 nexdv ⊢ ¬ A ∈ V ∧ B ∈ V ∧ w ∈ A N WWalksNOn G B → ¬ ∃ f f A SPathsOn ⁡ G B w
29 28 ralrimiva ⊢ ¬ A ∈ V ∧ B ∈ V → ∀ w ∈ A N WWalksNOn G B ¬ ∃ f f A SPathsOn ⁡ G B w
30 rabeq0 ⊢ w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w = ∅ ↔ ∀ w ∈ A N WWalksNOn G B ¬ ∃ f f A SPathsOn ⁡ G B w
31 29 30 sylibr ⊢ ¬ A ∈ V ∧ B ∈ V → w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w = ∅
32 24 31 eqtr4d ⊢ ¬ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w
33 14 adantr ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → N WSPathsNOn G = a ∈ V , b ∈ V ⟼ w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w
34 oveq12 ⊢ a = A ∧ b = B → a N WWalksNOn G b = A N WWalksNOn G B
35 oveq12 ⊢ a = A ∧ b = B → a SPathsOn ⁡ G b = A SPathsOn ⁡ G B
36 35 breqd ⊢ a = A ∧ b = B → f a SPathsOn ⁡ G b w ↔ f A SPathsOn ⁡ G B w
37 36 exbidv ⊢ a = A ∧ b = B → ∃ f f a SPathsOn ⁡ G b w ↔ ∃ f f A SPathsOn ⁡ G B w
38 34 37 rabeqbidv ⊢ a = A ∧ b = B → w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w
39 38 adantl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V ∧ a = A ∧ b = B → w ∈ a N WWalksNOn G b | ∃ f f a SPathsOn ⁡ G b w = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w
40 simprl ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → A ∈ V
41 simprr ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → B ∈ V
42 ovex ⊢ A N WWalksNOn G B ∈ V
43 42 rabex ⊢ w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w ∈ V
44 43 a1i ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w ∈ V
45 33 39 40 41 44 ovmpod ⊢ N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ V ∧ B ∈ V → A N WSPathsNOn G B = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w
46 13 32 45 ecase ⊢ A N WSPathsNOn G B = w ∈ A N WWalksNOn G B | ∃ f f A SPathsOn ⁡ G B w