Metamath Proof Explorer

Theorem 3wlkdlem4

Description: Lemma 4 for 3wlkd . (Contributed by Alexander van der Vekens, 11-Nov-2017) (Revised by AV, 7-Feb-2021)

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

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
2 3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3 3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
4 1 2 3 3wlkdlem3 ⊢ ( 𝜑 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) )
5 simpl ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( 𝑃 ‘ 0 ) = 𝐴 )
6 5 eleq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
7 simpr ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( 𝑃 ‘ 1 ) = 𝐵 )
8 7 eleq1d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( ( 𝑃 ‘ 1 ) ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
9 6 8 anbi12d ⊢ ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ( ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
10 9 biimparc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ) → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ) )
11 c0ex ⊢ 0 ∈ V
12 1ex ⊢ 1 ∈ V
13 11 12 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
14 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
15 14 eleq1d ⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
16 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
17 16 eleq1d ⊢ ( 𝑘 = 1 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 1 ) ∈ 𝑉 ) )
18 15 17 ralprg ⊢ ( ( 0 ∈ V ∧ 1 ∈ V ) → ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ) ) )
19 13 18 mp1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ) → ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 1 ) ∈ 𝑉 ) ) )
20 10 19 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ) → ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
21 20 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) → ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) )
22 simpl ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( 𝑃 ‘ 2 ) = 𝐶 )
23 22 eleq1d ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ↔ 𝐶 ∈ 𝑉 ) )
24 simpr ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( 𝑃 ‘ 3 ) = 𝐷 )
25 24 eleq1d ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( ( 𝑃 ‘ 3 ) ∈ 𝑉 ↔ 𝐷 ∈ 𝑉 ) )
26 23 25 anbi12d ⊢ ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ( ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 3 ) ∈ 𝑉 ) ↔ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
27 26 biimparc ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 3 ) ∈ 𝑉 ) )
28 2ex ⊢ 2 ∈ V
29 3ex ⊢ 3 ∈ V
30 28 29 pm3.2i ⊢ ( 2 ∈ V ∧ 3 ∈ V )
31 fveq2 ⊢ ( 𝑘 = 2 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 2 ) )
32 31 eleq1d ⊢ ( 𝑘 = 2 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 2 ) ∈ 𝑉 ) )
33 fveq2 ⊢ ( 𝑘 = 3 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 3 ) )
34 33 eleq1d ⊢ ( 𝑘 = 3 → ( ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( 𝑃 ‘ 3 ) ∈ 𝑉 ) )
35 32 34 ralprg ⊢ ( ( 2 ∈ V ∧ 3 ∈ V ) → ( ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 3 ) ∈ 𝑉 ) ) )
36 30 35 mp1i ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ∧ ( 𝑃 ‘ 3 ) ∈ 𝑉 ) ) )
37 27 36 mpbird ⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
38 37 ex ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) → ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) )
39 21 38 im2anan9 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) → ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ∧ ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) ) )
40 3 4 39 sylc ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ∧ ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) )
41 2 fveq2i ⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 𝐽 𝐾 𝐿 ”⟩ )
42 s3len ⊢ ( ♯ ‘ ⟨“ 𝐽 𝐾 𝐿 ”⟩ ) = 3
43 41 42 eqtri ⊢ ( ♯ ‘ 𝐹 ) = 3
44 43 oveq2i ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 3 )
45 fz0to3un2pr ⊢ ( 0 ... 3 ) = ( { 0 , 1 } ∪ { 2 , 3 } )
46 44 45 eqtri ⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( { 0 , 1 } ∪ { 2 , 3 } )
47 46 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )
48 ralunb ⊢ ( ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ∧ ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) )
49 47 48 bitri ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ↔ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ∧ ∀ 𝑘 ∈ { 2 , 3 } ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 ) )
50 40 49 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ 𝑉 )