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

Metamath Proof Explorer

Theorem 2wlklem

Description: Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018)

Ref Expression
Assertion 2wlklem ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1ex ⊢ 1 ∈ V
3 2fveq3 ⊢ ( 𝑘 = 0 → ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) )
4 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
5 fv0p1e1 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
6 4 5 preq12d ⊢ ( 𝑘 = 0 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
7 3 6 eqeq12d ⊢ ( 𝑘 = 0 → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
8 2fveq3 ⊢ ( 𝑘 = 1 → ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) )
9 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
10 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = ( 1 + 1 ) )
11 1p1e2 ⊢ ( 1 + 1 ) = 2
12 10 11 eqtrdi ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = 2 )
13 12 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 2 ) )
14 9 13 preq12d ⊢ ( 𝑘 = 1 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
15 8 14 eqeq12d ⊢ ( 𝑘 = 1 → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
16 1 2 7 15 ralpr ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )