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	biimtrdi	⊢ ( 𝐺 ∈ 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	biimtrdi	⊢ ( ( UPWalks ‘ 𝐺 ) = ∅ → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
16	11 15	syl	⊢ ( ¬ 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
17	10 16	pm2.61i	⊢ ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )