This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ) 𝐶 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )