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

Metamath Proof Explorer

Theorem 2wlkdlem4

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

Ref Expression
Hypotheses 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
Assertion 2wlkdlem4 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2 2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3 2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4 1 2 3 2wlkdlem3 ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )
5 simp1 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
6 5 eleq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
7 simp2 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 1 ) = 𝐵 )
8 7 eleq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝑃 ‘ 1 ) ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
9 simp3 ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( 𝑃 ‘ 2 ) = 𝐶 )
10 9 eleq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ↔ 𝐶 ∈ 𝑉 ) )
11 6 8 10 3anbi123d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) )
12 11 bicomd ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
13 4 12 syl ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) ) )
14 3 13 mpbid ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
15 2 fveq2i ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 𝐾 ”⟩ )
16 s2len ⊢ ( ♯ ‘ ⟨“ 𝐽 𝐾 ”⟩ ) = 2
17 15 16 eqtri ⊢ ( ♯ ‘ 𝐹 ) = 2
18 17 oveq2i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 2 )
19 fz0tp ⊢ ( 0 ... 2 ) = { 0 , 1 , 2 }
20 18 19 eqtri ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = { 0 , 1 , 2 }
21 20 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ∀ 𝑘 ∈ { 0 , 1 , 2 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
22 c0ex ⊢ 0 ∈ V
23 1ex ⊢ 1 ∈ V
24 2ex ⊢ 2 ∈ V
25 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
26 25 eleq1d ⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
27 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
28 27 eleq1d ⊢ ( 𝑘 = 1 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 1 ) ∈ 𝑉 ) )
29 fveq2 ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 2 ) )
30 29 eleq1d ⊢ ( 𝑘 = 2 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
31 22 23 24 26 28 30 raltp ⊢ ( ∀ 𝑘 ∈ { 0 , 1 , 2 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
32 21 31 bitri ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
33 14 32 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )