Metamath Proof Explorer

Theorem wlkswwlksf1o

Description: The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021)

Ref Expression
Hypothesis wlkswwlksf1o.f ⊢ 𝐹 = ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑤 ) )
Assertion wlkswwlksf1o ( 𝐺 ∈ USPGraph → 𝐹 : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 wlkswwlksf1o.f ⊢ 𝐹 = ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd ‘ 𝑤 ) )
2 fvex ⊢ ( 1st ‘ 𝑤 ) ∈ V
3 breq1 ⊢ ( 𝑓 = ( 1st ‘ 𝑤 ) → ( 𝑓 ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) ↔ ( 1st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) ) )
4 2 3 spcev ⊢ ( ( 1st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) → ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) )
5 wlkiswwlks ⊢ ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) ↔ ( 2nd ‘ 𝑤 ) ∈ ( WWalks ‘ 𝐺 ) ) )
6 4 5 imbitrid ⊢ ( 𝐺 ∈ USPGraph → ( ( 1st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) → ( 2nd ‘ 𝑤 ) ∈ ( WWalks ‘ 𝐺 ) ) )
7 wlkcpr ⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) )
8 7 biimpi ⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) → ( 1st ‘ 𝑤 ) ( Walks ‘ 𝐺 ) ( 2nd ‘ 𝑤 ) )
9 6 8 impel ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑤 ∈ ( Walks ‘ 𝐺 ) ) → ( 2nd ‘ 𝑤 ) ∈ ( WWalks ‘ 𝐺 ) )
10 9 1 fmptd ⊢ ( 𝐺 ∈ USPGraph → 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) )
11 simpr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) )
12 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑥 ) )
13 id ⊢ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) → 𝑥 ∈ ( Walks ‘ 𝐺 ) )
14 fvexd ⊢ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) → ( 2nd ‘ 𝑥 ) ∈ V )
15 1 12 13 14 fvmptd3 ⊢ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) → ( 𝐹 ‘ 𝑥 ) = ( 2nd ‘ 𝑥 ) )
16 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑦 ) )
17 id ⊢ ( 𝑦 ∈ ( Walks ‘ 𝐺 ) → 𝑦 ∈ ( Walks ‘ 𝐺 ) )
18 fvexd ⊢ ( 𝑦 ∈ ( Walks ‘ 𝐺 ) → ( 2nd ‘ 𝑦 ) ∈ V )
19 1 16 17 18 fvmptd3 ⊢ ( 𝑦 ∈ ( Walks ‘ 𝐺 ) → ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑦 ) )
20 15 19 eqeqan12d ⊢ ( ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) )
21 20 adantl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) )
22 uspgr2wlkeqi ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ∧ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
23 22 ad4ant134 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ) ∧ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
24 23 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ) → ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
25 21 24 sylbid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 ∈ ( Walks ‘ 𝐺 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
26 25 ralrimivva ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( Walks ‘ 𝐺 ) ∀ 𝑦 ∈ ( Walks ‘ 𝐺 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
27 dff13 ⊢ ( 𝐹 : ( Walks ‘ 𝐺 ) –1-1→ ( WWalks ‘ 𝐺 ) ↔ ( 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Walks ‘ 𝐺 ) ∀ 𝑦 ∈ ( Walks ‘ 𝐺 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
28 11 26 27 sylanbrc ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → 𝐹 : ( Walks ‘ 𝐺 ) –1-1→ ( WWalks ‘ 𝐺 ) )
29 wlkiswwlks ⊢ ( 𝐺 ∈ USPGraph → ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑦 ↔ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ) )
30 29 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑦 ↔ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ) )
31 df-br ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑦 ↔ ⟨ 𝑓 , 𝑦 ⟩ ∈ ( Walks ‘ 𝐺 ) )
32 vex ⊢ 𝑓 ∈ V
33 vex ⊢ 𝑦 ∈ V
34 32 33 op2nd ⊢ ( 2nd ‘ ⟨ 𝑓 , 𝑦 ⟩ ) = 𝑦
35 34 eqcomi ⊢ 𝑦 = ( 2nd ‘ ⟨ 𝑓 , 𝑦 ⟩ )
36 opex ⊢ ⟨ 𝑓 , 𝑦 ⟩ ∈ V
37 eleq1 ⊢ ( 𝑥 = ⟨ 𝑓 , 𝑦 ⟩ → ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ↔ ⟨ 𝑓 , 𝑦 ⟩ ∈ ( Walks ‘ 𝐺 ) ) )
38 fveq2 ⊢ ( 𝑥 = ⟨ 𝑓 , 𝑦 ⟩ → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ ⟨ 𝑓 , 𝑦 ⟩ ) )
39 38 eqeq2d ⊢ ( 𝑥 = ⟨ 𝑓 , 𝑦 ⟩ → ( 𝑦 = ( 2nd ‘ 𝑥 ) ↔ 𝑦 = ( 2nd ‘ ⟨ 𝑓 , 𝑦 ⟩ ) ) )
40 37 39 anbi12d ⊢ ( 𝑥 = ⟨ 𝑓 , 𝑦 ⟩ → ( ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ ⟨ 𝑓 , 𝑦 ⟩ ) ) ) )
41 36 40 spcev ⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ ⟨ 𝑓 , 𝑦 ⟩ ) ) → ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
42 35 41 mpan2 ⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( Walks ‘ 𝐺 ) → ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
43 31 42 sylbi ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑦 → ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
44 43 exlimiv ⊢ ( ∃ 𝑓 𝑓 ( Walks ‘ 𝐺 ) 𝑦 → ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
45 30 44 biimtrrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → ( 𝑦 ∈ ( WWalks ‘ 𝐺 ) → ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) ) )
46 45 imp ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ) → ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
47 df-rex ⊢ ( ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 2nd ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
48 46 47 sylibr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ) → ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 2nd ‘ 𝑥 ) )
49 15 eqeq2d ⊢ ( 𝑥 ∈ ( Walks ‘ 𝐺 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 = ( 2nd ‘ 𝑥 ) ) )
50 49 rexbiia ⊢ ( ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 2nd ‘ 𝑥 ) )
51 48 50 sylibr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ) → ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 𝐹 ‘ 𝑥 ) )
52 51 ralrimiva ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → ∀ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 𝐹 ‘ 𝑥 ) )
53 dffo3 ⊢ ( 𝐹 : ( Walks ‘ 𝐺 ) –onto→ ( WWalks ‘ 𝐺 ) ↔ ( 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( WWalks ‘ 𝐺 ) ∃ 𝑥 ∈ ( Walks ‘ 𝐺 ) 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
54 11 52 53 sylanbrc ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → 𝐹 : ( Walks ‘ 𝐺 ) –onto→ ( WWalks ‘ 𝐺 ) )
55 df-f1o ⊢ ( 𝐹 : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) ↔ ( 𝐹 : ( Walks ‘ 𝐺 ) –1-1→ ( WWalks ‘ 𝐺 ) ∧ 𝐹 : ( Walks ‘ 𝐺 ) –onto→ ( WWalks ‘ 𝐺 ) ) )
56 28 54 55 sylanbrc ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐹 : ( Walks ‘ 𝐺 ) ⟶ ( WWalks ‘ 𝐺 ) ) → 𝐹 : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )
57 10 56 mpdan ⊢ ( 𝐺 ∈ USPGraph → 𝐹 : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )