Metamath Proof Explorer


Theorem 4fvwrd4

Description: The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017)

Ref Expression
Assertion 4fvwrd4 ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 )
2 0nn0 0 ∈ ℕ0
3 elnn0uz ( 0 ∈ ℕ0 ↔ 0 ∈ ( ℤ ‘ 0 ) )
4 2 3 mpbi 0 ∈ ( ℤ ‘ 0 )
5 3nn0 3 ∈ ℕ0
6 elnn0uz ( 3 ∈ ℕ0 ↔ 3 ∈ ( ℤ ‘ 0 ) )
7 5 6 mpbi 3 ∈ ( ℤ ‘ 0 )
8 uzss ( 3 ∈ ( ℤ ‘ 0 ) → ( ℤ ‘ 3 ) ⊆ ( ℤ ‘ 0 ) )
9 7 8 ax-mp ( ℤ ‘ 3 ) ⊆ ( ℤ ‘ 0 )
10 9 sseli ( 𝐿 ∈ ( ℤ ‘ 3 ) → 𝐿 ∈ ( ℤ ‘ 0 ) )
11 eluzfz ( ( 0 ∈ ( ℤ ‘ 0 ) ∧ 𝐿 ∈ ( ℤ ‘ 0 ) ) → 0 ∈ ( 0 ... 𝐿 ) )
12 4 10 11 sylancr ( 𝐿 ∈ ( ℤ ‘ 3 ) → 0 ∈ ( 0 ... 𝐿 ) )
13 12 adantr ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → 0 ∈ ( 0 ... 𝐿 ) )
14 1 13 ffvelrnd ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
15 clel5 ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ↔ ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 )
16 14 15 sylib ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 )
17 1eluzge0 1 ∈ ( ℤ ‘ 0 )
18 1z 1 ∈ ℤ
19 3z 3 ∈ ℤ
20 1le3 1 ≤ 3
21 eluz2 ( 3 ∈ ( ℤ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 1 ≤ 3 ) )
22 18 19 20 21 mpbir3an 3 ∈ ( ℤ ‘ 1 )
23 uzss ( 3 ∈ ( ℤ ‘ 1 ) → ( ℤ ‘ 3 ) ⊆ ( ℤ ‘ 1 ) )
24 22 23 ax-mp ( ℤ ‘ 3 ) ⊆ ( ℤ ‘ 1 )
25 24 sseli ( 𝐿 ∈ ( ℤ ‘ 3 ) → 𝐿 ∈ ( ℤ ‘ 1 ) )
26 eluzfz ( ( 1 ∈ ( ℤ ‘ 0 ) ∧ 𝐿 ∈ ( ℤ ‘ 1 ) ) → 1 ∈ ( 0 ... 𝐿 ) )
27 17 25 26 sylancr ( 𝐿 ∈ ( ℤ ‘ 3 ) → 1 ∈ ( 0 ... 𝐿 ) )
28 27 adantr ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → 1 ∈ ( 0 ... 𝐿 ) )
29 1 28 ffvelrnd ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 )
30 clel5 ( ( 𝑃 ‘ 1 ) ∈ 𝑉 ↔ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 )
31 29 30 sylib ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 )
32 16 31 jca ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ( ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) )
33 2eluzge0 2 ∈ ( ℤ ‘ 0 )
34 uzuzle23 ( 𝐿 ∈ ( ℤ ‘ 3 ) → 𝐿 ∈ ( ℤ ‘ 2 ) )
35 eluzfz ( ( 2 ∈ ( ℤ ‘ 0 ) ∧ 𝐿 ∈ ( ℤ ‘ 2 ) ) → 2 ∈ ( 0 ... 𝐿 ) )
36 33 34 35 sylancr ( 𝐿 ∈ ( ℤ ‘ 3 ) → 2 ∈ ( 0 ... 𝐿 ) )
37 36 adantr ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → 2 ∈ ( 0 ... 𝐿 ) )
38 1 37 ffvelrnd ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 )
39 clel5 ( ( 𝑃 ‘ 2 ) ∈ 𝑉 ↔ ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 )
40 38 39 sylib ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 )
41 eluzfz ( ( 3 ∈ ( ℤ ‘ 0 ) ∧ 𝐿 ∈ ( ℤ ‘ 3 ) ) → 3 ∈ ( 0 ... 𝐿 ) )
42 7 41 mpan ( 𝐿 ∈ ( ℤ ‘ 3 ) → 3 ∈ ( 0 ... 𝐿 ) )
43 42 adantr ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → 3 ∈ ( 0 ... 𝐿 ) )
44 1 43 ffvelrnd ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 3 ) ∈ 𝑉 )
45 clel5 ( ( 𝑃 ‘ 3 ) ∈ 𝑉 ↔ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 )
46 44 45 sylib ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 )
47 32 40 46 jca32 ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ( ( ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
48 r19.42v ( ∃ 𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ∃ 𝑑𝑉 ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
49 r19.42v ( ∃ 𝑑𝑉 ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ↔ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) )
50 49 anbi2i ( ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ∃ 𝑑𝑉 ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
51 48 50 bitri ( ∃ 𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
52 51 rexbii ( ∃ 𝑐𝑉𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ∃ 𝑐𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
53 52 2rexbii ( ∃ 𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
54 r19.42v ( ∃ 𝑐𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ∃ 𝑐𝑉 ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
55 r19.41v ( ∃ 𝑐𝑉 ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ↔ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) )
56 55 anbi2i ( ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ∃ 𝑐𝑉 ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
57 54 56 bitri ( ∃ 𝑐𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
58 57 2rexbii ( ∃ 𝑎𝑉𝑏𝑉𝑐𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ∃ 𝑎𝑉𝑏𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
59 r19.41v ( ∃ 𝑏𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ∃ 𝑏𝑉 ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
60 r19.42v ( ∃ 𝑏𝑉 ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ↔ ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) )
61 60 anbi1i ( ( ∃ 𝑏𝑉 ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
62 59 61 bitri ( ∃ 𝑏𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
63 62 rexbii ( ∃ 𝑎𝑉𝑏𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ∃ 𝑎𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
64 r19.41v ( ∃ 𝑎𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ∃ 𝑎𝑉 ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
65 r19.41v ( ∃ 𝑎𝑉 ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ↔ ( ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) )
66 65 anbi1i ( ( ∃ 𝑎𝑉 ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
67 63 64 66 3bitri ( ∃ 𝑎𝑉𝑏𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
68 53 58 67 3bitri ( ∃ 𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) ↔ ( ( ∃ 𝑎𝑉 ( 𝑃 ‘ 0 ) = 𝑎 ∧ ∃ 𝑏𝑉 ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ∃ 𝑐𝑉 ( 𝑃 ‘ 2 ) = 𝑐 ∧ ∃ 𝑑𝑉 ( 𝑃 ‘ 3 ) = 𝑑 ) ) )
69 47 68 sylibr ( ( 𝐿 ∈ ( ℤ ‘ 3 ) ∧ 𝑃 : ( 0 ... 𝐿 ) ⟶ 𝑉 ) → ∃ 𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ( ( ( 𝑃 ‘ 0 ) = 𝑎 ∧ ( 𝑃 ‘ 1 ) = 𝑏 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝑐 ∧ ( 𝑃 ‘ 3 ) = 𝑑 ) ) )