Metamath Proof Explorer


Theorem isewlk

Description: Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion isewlk ( ( 𝐺𝑊𝑆 ∈ ℕ0*𝐹𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i 𝐼 = ( iEdg ‘ 𝐺 )
2 1 ewlksfval ( ( 𝐺𝑊𝑆 ∈ ℕ0* ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ) } )
3 2 3adant3 ( ( 𝐺𝑊𝑆 ∈ ℕ0*𝐹𝑈 ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ) } )
4 3 eleq2d ( ( 𝐺𝑊𝑆 ∈ ℕ0*𝐹𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ) } ) )
5 eleq1 ( 𝑓 = 𝐹 → ( 𝑓 ∈ Word dom 𝐼𝐹 ∈ Word dom 𝐼 ) )
6 fveq2 ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
7 6 oveq2d ( 𝑓 = 𝐹 → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
8 fveq1 ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑘 − 1 ) ) = ( 𝐹 ‘ ( 𝑘 − 1 ) ) )
9 8 fveq2d ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
10 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑘 ) = ( 𝐹𝑘 ) )
11 10 fveq2d ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓𝑘 ) ) = ( 𝐼 ‘ ( 𝐹𝑘 ) ) )
12 9 11 ineq12d ( 𝑓 = 𝐹 → ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) = ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) )
13 12 fveq2d ( 𝑓 = 𝐹 → ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) = ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) )
14 13 breq2d ( 𝑓 = 𝐹 → ( 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ↔ 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) )
15 7 14 raleqbidv ( 𝑓 = 𝐹 → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) )
16 5 15 anbi12d ( 𝑓 = 𝐹 → ( ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) ) )
17 16 elabg ( 𝐹𝑈 → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) ) )
18 17 3ad2ant3 ( ( 𝐺𝑊𝑆 ∈ ℕ0*𝐹𝑈 ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) ) )
19 4 18 bitrd ( ( 𝐺𝑊𝑆 ∈ ℕ0*𝐹𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) ) )