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

Metamath Proof Explorer

Theorem wlk2v2elem2

Description: Lemma 2 for wlk2v2e : The values of I after F are edges between two vertices enumerated by P . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)

Ref Expression
Hypotheses wlk2v2e.i ⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
wlk2v2e.f ⊢ 𝐹 = ⟨“ 0 0 ”⟩
wlk2v2e.x ⊢ 𝑋 ∈ V
wlk2v2e.y ⊢ 𝑌 ∈ V
wlk2v2e.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 𝑋 ”⟩
Assertion wlk2v2elem2 ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }

Proof

Step Hyp Ref Expression
1 wlk2v2e.i ⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
2 wlk2v2e.f ⊢ 𝐹 = ⟨“ 0 0 ”⟩
3 wlk2v2e.x ⊢ 𝑋 ∈ V
4 wlk2v2e.y ⊢ 𝑌 ∈ V
5 wlk2v2e.p ⊢ 𝑃 = ⟨“ 𝑋 𝑌 𝑋 ”⟩
6 2 fveq1i ⊢ ( 𝐹 ‘ 0 ) = ( ⟨“ 0 0 ”⟩ ‘ 0 )
7 0z ⊢ 0 ∈ ℤ
8 s2fv0 ⊢ ( 0 ∈ ℤ → ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0 )
9 7 8 ax-mp ⊢ ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0
10 6 9 eqtri ⊢ ( 𝐹 ‘ 0 ) = 0
11 10 fveq2i ⊢ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = ( 𝐼 ‘ 0 )
12 1 fveq1i ⊢ ( 𝐼 ‘ 0 ) = ( ⟨“ { 𝑋 , 𝑌 } ”⟩ ‘ 0 )
13 prex ⊢ { 𝑋 , 𝑌 } ∈ V
14 s1fv ⊢ ( { 𝑋 , 𝑌 } ∈ V → ( ⟨“ { 𝑋 , 𝑌 } ”⟩ ‘ 0 ) = { 𝑋 , 𝑌 } )
15 13 14 ax-mp ⊢ ( ⟨“ { 𝑋 , 𝑌 } ”⟩ ‘ 0 ) = { 𝑋 , 𝑌 }
16 12 15 eqtri ⊢ ( 𝐼 ‘ 0 ) = { 𝑋 , 𝑌 }
17 5 fveq1i ⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 0 )
18 s3fv0 ⊢ ( 𝑋 ∈ V → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 0 ) = 𝑋 )
19 3 18 ax-mp ⊢ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 0 ) = 𝑋
20 17 19 eqtri ⊢ ( 𝑃 ‘ 0 ) = 𝑋
21 5 fveq1i ⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 1 )
22 s3fv1 ⊢ ( 𝑌 ∈ V → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 1 ) = 𝑌 )
23 4 22 ax-mp ⊢ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 1 ) = 𝑌
24 21 23 eqtri ⊢ ( 𝑃 ‘ 1 ) = 𝑌
25 20 24 preq12i ⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝑋 , 𝑌 }
26 25 eqcomi ⊢ { 𝑋 , 𝑌 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) }
27 11 16 26 3eqtri ⊢ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) }
28 2 fveq1i ⊢ ( 𝐹 ‘ 1 ) = ( ⟨“ 0 0 ”⟩ ‘ 1 )
29 s2fv1 ⊢ ( 0 ∈ ℤ → ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0 )
30 7 29 ax-mp ⊢ ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0
31 28 30 eqtri ⊢ ( 𝐹 ‘ 1 ) = 0
32 31 fveq2i ⊢ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = ( 𝐼 ‘ 0 )
33 prcom ⊢ { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
34 5 fveq1i ⊢ ( 𝑃 ‘ 2 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 2 )
35 s3fv2 ⊢ ( 𝑋 ∈ V → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 2 ) = 𝑋 )
36 3 35 ax-mp ⊢ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 2 ) = 𝑋
37 34 36 eqtri ⊢ ( 𝑃 ‘ 2 ) = 𝑋
38 24 37 preq12i ⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { 𝑌 , 𝑋 }
39 38 eqcomi ⊢ { 𝑌 , 𝑋 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
40 33 39 eqtri ⊢ { 𝑋 , 𝑌 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
41 32 16 40 3eqtri ⊢ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
42 2wlklem ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
43 27 41 42 mpbir2an ⊢ ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }
44 5 2 2wlkdlem2 ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 }
45 44 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
46 43 45 mpbir ⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }