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 
|- ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> P : ( 0 ... L ) --> V )
2 0nn0 
 |-  0 e. NN0
3 elnn0uz 
 |-  ( 0 e. NN0 <-> 0 e. ( ZZ>= ` 0 ) )
4 2 3 mpbi 
 |-  0 e. ( ZZ>= ` 0 )
5 3nn0 
 |-  3 e. NN0
6 elnn0uz 
 |-  ( 3 e. NN0 <-> 3 e. ( ZZ>= ` 0 ) )
7 5 6 mpbi 
 |-  3 e. ( ZZ>= ` 0 )
8 uzss 
 |-  ( 3 e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 3 ) C_ ( ZZ>= ` 0 ) )
9 7 8 ax-mp 
 |-  ( ZZ>= ` 3 ) C_ ( ZZ>= ` 0 )
10 9 sseli 
 |-  ( L e. ( ZZ>= ` 3 ) -> L e. ( ZZ>= ` 0 ) )
11 eluzfz 
 |-  ( ( 0 e. ( ZZ>= ` 0 ) /\ L e. ( ZZ>= ` 0 ) ) -> 0 e. ( 0 ... L ) )
12 4 10 11 sylancr 
 |-  ( L e. ( ZZ>= ` 3 ) -> 0 e. ( 0 ... L ) )
13 12 adantr 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> 0 e. ( 0 ... L ) )
14 1 13 ffvelrnd 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> ( P ` 0 ) e. V )
15 clel5 
 |-  ( ( P ` 0 ) e. V <-> E. a e. V ( P ` 0 ) = a )
16 14 15 sylib 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. a e. V ( P ` 0 ) = a )
17 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
18 1z 
 |-  1 e. ZZ
19 3z 
 |-  3 e. ZZ
20 1le3 
 |-  1 <_ 3
21 eluz2 
 |-  ( 3 e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ 3 e. ZZ /\ 1 <_ 3 ) )
22 18 19 20 21 mpbir3an 
 |-  3 e. ( ZZ>= ` 1 )
23 uzss 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 3 ) C_ ( ZZ>= ` 1 ) )
24 22 23 ax-mp 
 |-  ( ZZ>= ` 3 ) C_ ( ZZ>= ` 1 )
25 24 sseli 
 |-  ( L e. ( ZZ>= ` 3 ) -> L e. ( ZZ>= ` 1 ) )
26 eluzfz 
 |-  ( ( 1 e. ( ZZ>= ` 0 ) /\ L e. ( ZZ>= ` 1 ) ) -> 1 e. ( 0 ... L ) )
27 17 25 26 sylancr 
 |-  ( L e. ( ZZ>= ` 3 ) -> 1 e. ( 0 ... L ) )
28 27 adantr 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> 1 e. ( 0 ... L ) )
29 1 28 ffvelrnd 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> ( P ` 1 ) e. V )
30 clel5 
 |-  ( ( P ` 1 ) e. V <-> E. b e. V ( P ` 1 ) = b )
31 29 30 sylib 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. b e. V ( P ` 1 ) = b )
32 16 31 jca 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> ( E. a e. V ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) )
33 2eluzge0 
 |-  2 e. ( ZZ>= ` 0 )
34 uzuzle23 
 |-  ( L e. ( ZZ>= ` 3 ) -> L e. ( ZZ>= ` 2 ) )
35 eluzfz 
 |-  ( ( 2 e. ( ZZ>= ` 0 ) /\ L e. ( ZZ>= ` 2 ) ) -> 2 e. ( 0 ... L ) )
36 33 34 35 sylancr 
 |-  ( L e. ( ZZ>= ` 3 ) -> 2 e. ( 0 ... L ) )
37 36 adantr 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> 2 e. ( 0 ... L ) )
38 1 37 ffvelrnd 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> ( P ` 2 ) e. V )
39 clel5 
 |-  ( ( P ` 2 ) e. V <-> E. c e. V ( P ` 2 ) = c )
40 38 39 sylib 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. c e. V ( P ` 2 ) = c )
41 eluzfz 
 |-  ( ( 3 e. ( ZZ>= ` 0 ) /\ L e. ( ZZ>= ` 3 ) ) -> 3 e. ( 0 ... L ) )
42 7 41 mpan 
 |-  ( L e. ( ZZ>= ` 3 ) -> 3 e. ( 0 ... L ) )
43 42 adantr 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> 3 e. ( 0 ... L ) )
44 1 43 ffvelrnd 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> ( P ` 3 ) e. V )
45 clel5 
 |-  ( ( P ` 3 ) e. V <-> E. d e. V ( P ` 3 ) = d )
46 44 45 sylib 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. d e. V ( P ` 3 ) = d )
47 32 40 46 jca32 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> ( ( E. a e. V ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
48 r19.42v 
 |-  ( E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ E. d e. V ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) )
49 r19.42v 
 |-  ( E. d e. V ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) <-> ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) )
50 49 anbi2i 
 |-  ( ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ E. d e. V ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
51 48 50 bitri 
 |-  ( E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
52 51 rexbii 
 |-  ( E. c e. V E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) <-> E. c e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
53 52 2rexbii 
 |-  ( E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) <-> E. a e. V E. b e. V E. c e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
54 r19.42v 
 |-  ( E. c e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ E. c e. V ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
55 r19.41v 
 |-  ( E. c e. V ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) <-> ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) )
56 55 anbi2i 
 |-  ( ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ E. c e. V ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
57 54 56 bitri 
 |-  ( E. c e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
58 57 2rexbii 
 |-  ( E. a e. V E. b e. V E. c e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> E. a e. V E. b e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
59 r19.41v 
 |-  ( E. b e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( E. b e. V ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
60 r19.42v 
 |-  ( E. b e. V ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) <-> ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) )
61 60 anbi1i 
 |-  ( ( E. b e. V ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
62 59 61 bitri 
 |-  ( E. b e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
63 62 rexbii 
 |-  ( E. a e. V E. b e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> E. a e. V ( ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
64 r19.41v 
 |-  ( E. a e. V ( ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( E. a e. V ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
65 r19.41v 
 |-  ( E. a e. V ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) <-> ( E. a e. V ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) )
66 65 anbi1i 
 |-  ( ( E. a e. V ( ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( E. a e. V ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
67 63 64 66 3bitri 
 |-  ( E. a e. V E. b e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) <-> ( ( E. a e. V ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
68 53 58 67 3bitri 
 |-  ( E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) <-> ( ( E. a e. V ( P ` 0 ) = a /\ E. b e. V ( P ` 1 ) = b ) /\ ( E. c e. V ( P ` 2 ) = c /\ E. d e. V ( P ` 3 ) = d ) ) )
69 47 68 sylibr 
 |-  ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) )