Metamath Proof Explorer


Theorem upwlkbprop

Description: Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 29-Dec-2020)

Ref Expression
Hypotheses upwlksfval.v 𝑉 = ( Vtx ‘ 𝐺 )
upwlksfval.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion upwlkbprop ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )

Proof

Step Hyp Ref Expression
1 upwlksfval.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upwlksfval.i 𝐼 = ( iEdg ‘ 𝐺 )
3 1 2 upwlksfval ( 𝐺 ∈ V → ( UPWalks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } )
4 3 breqd ( 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } 𝑃 ) )
5 brabv ( 𝐹 { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
6 4 5 syl6bi ( 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
7 6 imdistani ( ( 𝐺 ∈ V ∧ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) → ( 𝐺 ∈ V ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
8 3anass ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ↔ ( 𝐺 ∈ V ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
9 7 8 sylibr ( ( 𝐺 ∈ V ∧ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
10 9 ex ( 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
11 fvprc ( ¬ 𝐺 ∈ V → ( UPWalks ‘ 𝐺 ) = ∅ )
12 breq ( ( UPWalks ‘ 𝐺 ) = ∅ → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃𝐹𝑃 ) )
13 br0 ¬ 𝐹𝑃
14 13 pm2.21i ( 𝐹𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
15 12 14 syl6bi ( ( UPWalks ‘ 𝐺 ) = ∅ → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
16 11 15 syl ( ¬ 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
17 10 16 pm2.61i ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )