Theorem wwlksonvtx

Description: If a word W represents a walk of length 2 on two classes A and C , these classes are vertices. (Contributed by AV, 14-Mar-2022)

	Ref	Expression
Hypothesis	wwlksonvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	wwlksonvtx	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		wwlksonvtx.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fvex	⊢ ( Vtx ‘ 𝑔 ) ∈ V
3	2 2	pm3.2i	⊢ ( ( Vtx ‘ 𝑔 ) ∈ V ∧ ( Vtx ‘ 𝑔 ) ∈ V )
4	3	rgen2w	⊢ ∀ 𝑛 ∈ ℕ0 ∀ 𝑔 ∈ V ( ( Vtx ‘ 𝑔 ) ∈ V ∧ ( Vtx ‘ 𝑔 ) ∈ V )
5		df-wwlksnon	⊢ WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )
6		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
7	6 6	jca	⊢ ( 𝑔 = 𝐺 → ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) )
8	7	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ∧ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) ) )
9	5 8	el2mpocl	⊢ ( ∀ 𝑛 ∈ ℕ0 ∀ 𝑔 ∈ V ( ( Vtx ‘ 𝑔 ) ∈ V ∧ ( Vtx ‘ 𝑔 ) ∈ V ) → ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐶 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) )
10	4 9	ax-mp	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐶 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) )
11	1	eleq2i	⊢ ( 𝐴 ∈ 𝑉 ↔ 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
12	1	eleq2i	⊢ ( 𝐶 ∈ 𝑉 ↔ 𝐶 ∈ ( Vtx ‘ 𝐺 ) )
13	11 12	anbi12i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) )
14	13	biimpri	⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
15	10 14	simpl2im	⊢ ( 𝑊 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )