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 \in ℤ_{\geq 3} \land P : (0 \dots L) ⟶ V) \to \exists a \in V \exists b \in V \exists c \in V \exists d \in V ((P (0) = a \land P (1) = b) \land (P (2) = c \land P (3) = d))$

Proof

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

Metamath Proof Explorer

Theorem 4fvwrd4

Proof