Metamath Proof Explorer

Theorem 2wlkdlem10

Description: Lemma 10 for 3wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
2wlkd.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
2wlkd.e ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
Assertion 2wlkdlem10 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2 2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3 2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4 2wlkd.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) )
5 2wlkd.e ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ) )
6 1 2 3 4 5 2wlkdlem9 ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) )
7 1 2 3 2wlkdlem3 ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )
8 preq12 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝐴 , 𝐵 } )
9 8 3adant3 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝐴 , 𝐵 } )
10 9 sseq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
11 preq12 ⊢ ( ( ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { 𝐵 , 𝐶 } )
12 11 3adant1 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { 𝐵 , 𝐶 } )
13 12 sseq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ↔ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) )
14 10 13 anbi12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) ↔ ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) ) )
15 7 14 syl ⊢ ( 𝜑 → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) ↔ ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) ) )
16 6 15 mpbird ⊢ ( 𝜑 → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) )
17 1 2 2wlkdlem2 ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 }
18 17 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ { 0 , 1 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
19 c0ex ⊢ 0 ∈ V
20 1ex ⊢ 1 ∈ V
21 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
22 fv0p1e1 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
23 21 22 preq12d ⊢ ( 𝑘 = 0 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
24 2fveq3 ⊢ ( 𝑘 = 0 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) )
25 23 24 sseq12d ⊢ ( 𝑘 = 0 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ) )
26 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
27 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = ( 1 + 1 ) )
28 1p1e2 ⊢ ( 1 + 1 ) = 2
29 27 28 eqtrdi ⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = 2 )
30 29 fveq2d ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 2 ) )
31 26 30 preq12d ⊢ ( 𝑘 = 1 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
32 2fveq3 ⊢ ( 𝑘 = 1 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) )
33 31 32 sseq12d ⊢ ( 𝑘 = 1 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) )
34 19 20 25 33 ralpr ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) )
35 18 34 bitri ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) ) )
36 16 35 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )