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