Metamath Proof Explorer


Theorem wlknwwlksnbij

Description: The mapping ( t e. T |-> ( 2ndt ) ) is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 5-Aug-2022)

Ref Expression
Hypotheses wlknwwlksnbij.t 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 }
wlknwwlksnbij.w 𝑊 = ( 𝑁 WWalksN 𝐺 )
wlknwwlksnbij.f 𝐹 = ( 𝑡𝑇 ↦ ( 2nd𝑡 ) )
Assertion wlknwwlksnbij ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝐹 : 𝑇1-1-onto𝑊 )

Proof

Step Hyp Ref Expression
1 wlknwwlksnbij.t 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 }
2 wlknwwlksnbij.w 𝑊 = ( 𝑁 WWalksN 𝐺 )
3 wlknwwlksnbij.f 𝐹 = ( 𝑡𝑇 ↦ ( 2nd𝑡 ) )
4 eqid ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) = ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) )
5 4 wlkswwlksf1o ( 𝐺 ∈ USPGraph → ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )
6 5 adantr ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) : ( Walks ‘ 𝐺 ) –1-1-onto→ ( WWalks ‘ 𝐺 ) )
7 fveqeq2 ( 𝑞 = ( 2nd𝑝 ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ) )
8 7 3ad2ant3 ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2nd𝑝 ) ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ) )
9 wlkcpr ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) )
10 wlklenvp1 ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) → ( ♯ ‘ ( 2nd𝑝 ) ) = ( ( ♯ ‘ ( 1st𝑝 ) ) + 1 ) )
11 eqeq1 ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( ( ♯ ‘ ( 1st𝑝 ) ) + 1 ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ( ♯ ‘ ( 1st𝑝 ) ) + 1 ) = ( 𝑁 + 1 ) ) )
12 wlkcl ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) → ( ♯ ‘ ( 1st𝑝 ) ) ∈ ℕ0 )
13 12 nn0cnd ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) → ( ♯ ‘ ( 1st𝑝 ) ) ∈ ℂ )
14 13 adantr ( ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → ( ♯ ‘ ( 1st𝑝 ) ) ∈ ℂ )
15 nn0cn ( 𝑁 ∈ ℕ0𝑁 ∈ ℂ )
16 15 adantl ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
17 16 adantl ( ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → 𝑁 ∈ ℂ )
18 1cnd ( ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → 1 ∈ ℂ )
19 14 17 18 addcan2d ( ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) → ( ( ( ♯ ‘ ( 1st𝑝 ) ) + 1 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) )
20 11 19 sylan9bbr ( ( ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) ∧ ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ) ∧ ( ♯ ‘ ( 2nd𝑝 ) ) = ( ( ♯ ‘ ( 1st𝑝 ) ) + 1 ) ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) )
21 20 exp31 ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( ( ♯ ‘ ( 1st𝑝 ) ) + 1 ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) ) ) )
22 10 21 mpid ( ( 1st𝑝 ) ( Walks ‘ 𝐺 ) ( 2nd𝑝 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) ) )
23 9 22 sylbi ( 𝑝 ∈ ( Walks ‘ 𝐺 ) → ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) ) )
24 23 impcom ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) )
25 24 3adant3 ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2nd𝑝 ) ) → ( ( ♯ ‘ ( 2nd𝑝 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) )
26 8 25 bitrd ( ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑝 ∈ ( Walks ‘ 𝐺 ) ∧ 𝑞 = ( 2nd𝑝 ) ) → ( ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 ) )
27 4 6 26 f1oresrab ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } –1-1-onto→ { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
28 1 mpteq1i ( 𝑡𝑇 ↦ ( 2nd𝑡 ) ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ↦ ( 2nd𝑡 ) )
29 ssrab2 { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ⊆ ( Walks ‘ 𝐺 )
30 resmpt ( { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ⊆ ( Walks ‘ 𝐺 ) → ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ↦ ( 2nd𝑡 ) ) )
31 29 30 ax-mp ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) = ( 𝑡 ∈ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ↦ ( 2nd𝑡 ) )
32 fveq2 ( 𝑡 = 𝑝 → ( 2nd𝑡 ) = ( 2nd𝑝 ) )
33 32 cbvmptv ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑡 ) ) = ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) )
34 33 reseq1i ( ( 𝑡 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑡 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } )
35 28 31 34 3eqtr2i ( 𝑡𝑇 ↦ ( 2nd𝑡 ) ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } )
36 35 a1i ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑡𝑇 ↦ ( 2nd𝑡 ) ) = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) )
37 3 36 syl5eq ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) )
38 1 a1i ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝑇 = { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } )
39 wwlksn ( 𝑁 ∈ ℕ0 → ( 𝑁 WWalksN 𝐺 ) = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
40 39 adantl ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 WWalksN 𝐺 ) = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
41 2 40 syl5eq ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝑊 = { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } )
42 37 38 41 f1oeq123d ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 : 𝑇1-1-onto𝑊 ↔ ( ( 𝑝 ∈ ( Walks ‘ 𝐺 ) ↦ ( 2nd𝑝 ) ) ↾ { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } ) : { 𝑝 ∈ ( Walks ‘ 𝐺 ) ∣ ( ♯ ‘ ( 1st𝑝 ) ) = 𝑁 } –1-1-onto→ { 𝑞 ∈ ( WWalks ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑞 ) = ( 𝑁 + 1 ) } ) )
43 27 42 mpbird ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0 ) → 𝐹 : 𝑇1-1-onto𝑊 )