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

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 ffvelcdmd ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 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 ffvelcdmd ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 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 ffvelcdmd ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 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 ffvelcdmd ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 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 ) = 𝑑 ) ) )