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 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )