Theorem umgr2adedgwlkon

Description: In a multigraph, two adjacent edges form a walk between two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021)

	Ref	Expression
Hypotheses	umgr2adedgwlk.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	umgr2adedgwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	umgr2adedgwlk.f	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
	umgr2adedgwlk.p	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
	umgr2adedgwlk.g	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
	umgr2adedgwlk.a	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
	umgr2adedgwlk.j	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } )
	umgr2adedgwlk.k	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } )
Assertion	umgr2adedgwlkon	⊢ ( 𝜑 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		umgr2adedgwlk.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		umgr2adedgwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		umgr2adedgwlk.f	⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
4		umgr2adedgwlk.p	⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
5		umgr2adedgwlk.g	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
6		umgr2adedgwlk.a	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
7		umgr2adedgwlk.j	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } )
8		umgr2adedgwlk.k	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } )
9		3anass	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐺 ∈ UMGraph ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) )
10	5 6 9	sylanbrc	⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
11	1	umgr2adedgwlklem	⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
12	10 11	syl	⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
13	12	simprd	⊢ ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
14	12	simpld	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
15		ssid	⊢ { 𝐴 , 𝐵 } ⊆ { 𝐴 , 𝐵 }
16	15 7	sseqtrrid	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) )
17		ssid	⊢ { 𝐵 , 𝐶 } ⊆ { 𝐵 , 𝐶 }
18	17 8	sseqtrrid	⊢ ( 𝜑 → { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) )
19	16 18	jca	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
20		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
21	4 3 13 14 19 20 2	2wlkond	⊢ ( 𝜑 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 )