Metamath Proof Explorer

Theorem wwlksnextbij

Description: There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij.v ⊢ V = Vtx ⁡ G
wwlksnextbij.e ⊢ E = Edg ⁡ G
Assertion wwlksnextbij ⊢ W ∈ N WWalksN G → ∃ f f : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E

Proof

Step Hyp Ref Expression
1 wwlksnextbij.v ⊢ V = Vtx ⁡ G
2 wwlksnextbij.e ⊢ E = Edg ⁡ G
3 ovexd ⊢ W ∈ N WWalksN G → N + 1 WWalksN G ∈ V
4 rabexg ⊢ N + 1 WWalksN G ∈ V → t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ∈ V
5 mptexg ⊢ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ∈ V → x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x ∈ V
6 3 4 5 3syl ⊢ W ∈ N WWalksN G → x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x ∈ V
7 eqid ⊢ w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
8 preq2 ⊢ n = p → lastS ⁡ W n = lastS ⁡ W p
9 8 eleq1d ⊢ n = p → lastS ⁡ W n ∈ E ↔ lastS ⁡ W p ∈ E
10 9 cbvrabv ⊢ n ∈ V | lastS ⁡ W n ∈ E = p ∈ V | lastS ⁡ W p ∈ E
11 fveqeq2 ⊢ t = w → t = N + 2 ↔ w = N + 2
12 oveq1 ⊢ t = w → t prefix N + 1 = w prefix N + 1
13 12 eqeq1d ⊢ t = w → t prefix N + 1 = W ↔ w prefix N + 1 = W
14 fveq2 ⊢ t = w → lastS ⁡ t = lastS ⁡ w
15 14 preq2d ⊢ t = w → lastS ⁡ W lastS ⁡ t = lastS ⁡ W lastS ⁡ w
16 15 eleq1d ⊢ t = w → lastS ⁡ W lastS ⁡ t ∈ E ↔ lastS ⁡ W lastS ⁡ w ∈ E
17 11 13 16 3anbi123d ⊢ t = w → t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ↔ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
18 17 cbvrabv ⊢ t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
19 18 mpteq1i ⊢ x ∈ t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x = x ∈ w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟼ lastS ⁡ x
20 1 2 7 10 19 wwlksnextbij0 ⊢ W ∈ N WWalksN G → x ∈ t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x : w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E
21 eqid ⊢ t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E = t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E
22 1 2 21 wwlksnextwrd ⊢ W ∈ N WWalksN G → t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E = t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E
23 22 eqcomd ⊢ W ∈ N WWalksN G → t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E = t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E
24 23 mpteq1d ⊢ W ∈ N WWalksN G → x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x = x ∈ t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x
25 1 2 7 wwlksnextwrd ⊢ W ∈ N WWalksN G → w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
26 25 eqcomd ⊢ W ∈ N WWalksN G → w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
27 eqidd ⊢ W ∈ N WWalksN G → n ∈ V | lastS ⁡ W n ∈ E = n ∈ V | lastS ⁡ W n ∈ E
28 24 26 27 f1oeq123d ⊢ W ∈ N WWalksN G → x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E ↔ x ∈ t ∈ Word V | t = N + 2 ∧ t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x : w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E
29 20 28 mpbird ⊢ W ∈ N WWalksN G → x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E
30 f1oeq1 ⊢ f = x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x → f : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E ↔ x ∈ t ∈ N + 1 WWalksN G | t prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ t ∈ E ⟼ lastS ⁡ x : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E
31 6 29 30 spcedv ⊢ W ∈ N WWalksN G → ∃ f f : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E