Metamath Proof Explorer

Theorem upgrwlkdvspth

Description: A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk . (Contributed by Alexander van der Vekens, 27-Oct-2017) (Revised by AV, 17-Jan-2021)

Ref Expression
Assertion upgrwlkdvspth ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 3simpc ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
2 upgrspthswlk ⊢ ( 𝐺 ∈ UPGraph → ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } )
3 2 3ad2ant1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( SPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } )
4 3 breqd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } 𝑃 ) )
5 wlkv ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
6 3simpc ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
7 5 6 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
8 7 3ad2ant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
9 breq12 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ↔ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) )
10 cnveq ⊢ ( 𝑝 = 𝑃 → ◡ 𝑝 = ◡ 𝑃 )
11 10 funeqd ⊢ ( 𝑝 = 𝑃 → ( Fun ◡ 𝑝 ↔ Fun ◡ 𝑃 ) )
12 11 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( Fun ◡ 𝑝 ↔ Fun ◡ 𝑃 ) )
13 9 12 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
14 eqid ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) }
15 13 14 brabga ⊢ ( ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
16 8 15 syl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ Fun ◡ 𝑝 ) } 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
17 4 16 bitrd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ) )
18 1 17 mpbird ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )