s3rex

Description: Membership in a family of words of length 3. (Contributed by Thierry Arnoux, 23-Aug-2026)

		Ref	Expression
	Hypothesis	s3rex.1	$⊢ S \in V$
	Assertion	s3rex	$⊢ A \in (S^{(0 ..^3)}) \leftrightarrow \exists x \in S \exists y \in S \exists z \in S A = ⟨“ x y z ”⟩$

Proof

Step	Hyp	Ref	Expression
1		s3rex.1	$⊢ S \in V$
2		id	$⊢ x = A (0) \to x = A (0)$
3		eqidd	$⊢ x = A (0) \to y = y$
4		eqidd	$⊢ x = A (0) \to z = z$
5	2 3 4	s3eqd	$⊢ x = A (0) \to ⟨“ x y z ”⟩ = ⟨“ A (0) y z ”⟩$
6	5	eqeq2d	$⊢ x = A (0) \to (A = ⟨“ x y z ”⟩ \leftrightarrow A = ⟨“ A (0) y z ”⟩)$
7		s3eq2	$⊢ y = A (1) \to ⟨“ A (0) y z ”⟩ = ⟨“ A (0) A (1) z ”⟩$
8	7	eqeq2d	$⊢ y = A (1) \to (A = ⟨“ A (0) y z ”⟩ \leftrightarrow A = ⟨“ A (0) A (1) z ”⟩)$
9		eqidd	$⊢ z = A (2) \to A (0) = A (0)$
10		eqidd	$⊢ z = A (2) \to A (1) = A (1)$
11		id	$⊢ z = A (2) \to z = A (2)$
12	9 10 11	s3eqd	$⊢ z = A (2) \to ⟨“ A (0) A (1) z ”⟩ = ⟨“ A (0) A (1) A (2) ”⟩$
13	12	eqeq2d	$⊢ z = A (2) \to (A = ⟨“ A (0) A (1) z ”⟩ \leftrightarrow A = ⟨“ A (0) A (1) A (2) ”⟩)$
14		elmapi	$⊢ A \in (S^{(0 ..^3)}) \to A : (0 ..^3) ⟶ S$
15		c0ex	$⊢ 0 \in V$
16	15	tpid1	$⊢ 0 \in \{0, 1, 2\}$
17		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
18	16 17	eleqtrri	$⊢ 0 \in (0 ..^3)$
19	18	a1i	$⊢ A \in (S^{(0 ..^3)}) \to 0 \in (0 ..^3)$
20	14 19	ffvelcdmd	$⊢ A \in (S^{(0 ..^3)}) \to A (0) \in S$
21		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
22	21 17	eleqtrri	$⊢ 1 \in (0 ..^3)$
23	22	a1i	$⊢ A \in (S^{(0 ..^3)}) \to 1 \in (0 ..^3)$
24	14 23	ffvelcdmd	$⊢ A \in (S^{(0 ..^3)}) \to A (1) \in S$
25		2ex	$⊢ 2 \in V$
26	25	tpid3	$⊢ 2 \in \{0, 1, 2\}$
27	26 17	eleqtrri	$⊢ 2 \in (0 ..^3)$
28	27	a1i	$⊢ A \in (S^{(0 ..^3)}) \to 2 \in (0 ..^3)$
29	14 28	ffvelcdmd	$⊢ A \in (S^{(0 ..^3)}) \to A (2) \in S$
30		iswrdi	$⊢ A : (0 ..^3) ⟶ S \to A \in Word S$
31	14 30	syl	$⊢ A \in (S^{(0 ..^3)}) \to A \in Word S$
32		elmapfn	$⊢ A \in (S^{(0 ..^3)}) \to A Fn (0 ..^3)$
33		hashfn	$⊢ A Fn (0 ..^3) \to \|A\| = \|(0 ..^3)\|$
34	32 33	syl	$⊢ A \in (S^{(0 ..^3)}) \to \|A\| = \|(0 ..^3)\|$
35		3nn0	$⊢ 3 \in ℕ_{0}$
36		hashfzo0	$⊢ 3 \in ℕ_{0} \to \|(0 ..^3)\| = 3$
37	35 36	ax-mp	$⊢ \|(0 ..^3)\| = 3$
38	34 37	eqtrdi	$⊢ A \in (S^{(0 ..^3)}) \to \|A\| = 3$
39		wrdlen3s3	$⊢ (A \in Word S \land \|A\| = 3) \to A = ⟨“ A (0) A (1) A (2) ”⟩$
40	31 38 39	syl2anc	$⊢ A \in (S^{(0 ..^3)}) \to A = ⟨“ A (0) A (1) A (2) ”⟩$
41	6 8 13 20 24 29 40	3rspcedvdw	$⊢ A \in (S^{(0 ..^3)}) \to \exists x \in S \exists y \in S \exists z \in S A = ⟨“ x y z ”⟩$
42	1	a1i	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to S \in V$
43		ovexd	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to (0 ..^3) \in V$
44		simpr	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to A = ⟨“ x y z ”⟩$
45	44	fveq2d	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to \|A\| = \|⟨“ x y z ”⟩\|$
46		s3len	$⊢ \|⟨“ x y z ”⟩\| = 3$
47	45 46	eqtr2di	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to 3 = \|A\|$
48		simplll	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to x \in S$
49		simpllr	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to y \in S$
50		simplr	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to z \in S$
51	48 49 50	s3cld	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to ⟨“ x y z ”⟩ \in Word S$
52	44 51	eqeltrd	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to A \in Word S$
53	47 52	wrdfd	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to A : (0 ..^3) ⟶ S$
54	42 43 53	elmapdd	$⊢ (((x \in S \land y \in S) \land z \in S) \land A = ⟨“ x y z ”⟩) \to A \in (S^{(0 ..^3)})$
55	54	rexlimdva2	$⊢ (x \in S \land y \in S) \to (\exists z \in S A = ⟨“ x y z ”⟩ \to A \in (S^{(0 ..^3)}))$
56	55	rexlimivv	$⊢ \exists x \in S \exists y \in S \exists z \in S A = ⟨“ x y z ”⟩ \to A \in (S^{(0 ..^3)})$
57	41 56	impbii	$⊢ A \in (S^{(0 ..^3)}) \leftrightarrow \exists x \in S \exists y \in S \exists z \in S A = ⟨“ x y z ”⟩$

Metamath Proof Explorer

Theorem s3rex

Proof