reuccatpfxs1

Description: There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Revised by AV, 13-Oct-2022)

		Ref	Expression
	Hypothesis	reuccatpfxs1.1	$⊢ \underline{Ⅎ} v X$
	Assertion	reuccatpfxs1	$⊢ (W \in Word V \land \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1)) \to (\exists! v \in V W ++ ⟨“ v ”⟩ \in X \to \exists! x \in X W = x prefix \|W\|)$

Proof

Step	Hyp	Ref	Expression
1		reuccatpfxs1.1	$⊢ \underline{Ⅎ} v X$
2		eleq1w	$⊢ x = y \to (x \in Word V \leftrightarrow y \in Word V)$
3		fveqeq2	$⊢ x = y \to (\|x\| = \|W\| + 1 \leftrightarrow \|y\| = \|W\| + 1)$
4	2 3	anbi12d	$⊢ x = y \to ((x \in Word V \land \|x\| = \|W\| + 1) \leftrightarrow (y \in Word V \land \|y\| = \|W\| + 1))$
5	4	cbvralvw	$⊢ \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1) \leftrightarrow \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)$
6	1	nfel2	$⊢ Ⅎ v W ++ ⟨“ u ”⟩ \in X$
7	1	nfel2	$⊢ Ⅎ v W ++ ⟨“ x ”⟩ \in X$
8		s1eq	$⊢ v = x \to ⟨“ v ”⟩ = ⟨“ x ”⟩$
9	8	oveq2d	$⊢ v = x \to W ++ ⟨“ v ”⟩ = W ++ ⟨“ x ”⟩$
10	9	eleq1d	$⊢ v = x \to (W ++ ⟨“ v ”⟩ \in X \leftrightarrow W ++ ⟨“ x ”⟩ \in X)$
11		s1eq	$⊢ x = u \to ⟨“ x ”⟩ = ⟨“ u ”⟩$
12	11	oveq2d	$⊢ x = u \to W ++ ⟨“ x ”⟩ = W ++ ⟨“ u ”⟩$
13	12	eleq1d	$⊢ x = u \to (W ++ ⟨“ x ”⟩ \in X \leftrightarrow W ++ ⟨“ u ”⟩ \in X)$
14	6 7 10 13	reu8nf	$⊢ \exists! v \in V W ++ ⟨“ v ”⟩ \in X \leftrightarrow \exists v \in V (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))$
15		nfv	$⊢ Ⅎ v W \in Word V$
16		nfv	$⊢ Ⅎ v (y \in Word V \land \|y\| = \|W\| + 1)$
17	1 16	nfralw	$⊢ Ⅎ v \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)$
18	15 17	nfan	$⊢ Ⅎ v (W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1))$
19		nfv	$⊢ Ⅎ v W = x prefix \|W\|$
20	1 19	nfreuw	$⊢ Ⅎ v \exists! x \in X W = x prefix \|W\|$
21		simprl	$⊢ (((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \to W ++ ⟨“ v ”⟩ \in X$
22		simpl	$⊢ (W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \to W \in Word V$
23	22	ad2antrr	$⊢ (((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \to W \in Word V$
24	23	anim1i	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to (W \in Word V \land x \in X)$
25		simplrr	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u)$
26		simp-4r	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)$
27		reuccatpfxs1lem	$⊢ ((W \in Word V \land x \in X) \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u) \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \to (W = x prefix \|W\| \to x = W ++ ⟨“ v ”⟩)$
28	24 25 26 27	syl3anc	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to (W = x prefix \|W\| \to x = W ++ ⟨“ v ”⟩)$
29		oveq1	$⊢ x = W ++ ⟨“ v ”⟩ \to x prefix \|W\| = (W ++ ⟨“ v ”⟩) prefix \|W\|$
30		s1cl	$⊢ v \in V \to ⟨“ v ”⟩ \in Word V$
31	22 30	anim12i	$⊢ ((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \to (W \in Word V \land ⟨“ v ”⟩ \in Word V)$
32	31	ad2antrr	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to (W \in Word V \land ⟨“ v ”⟩ \in Word V)$
33		pfxccat1	$⊢ (W \in Word V \land ⟨“ v ”⟩ \in Word V) \to (W ++ ⟨“ v ”⟩) prefix \|W\| = W$
34	32 33	syl	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to (W ++ ⟨“ v ”⟩) prefix \|W\| = W$
35	29 34	sylan9eqr	$⊢ (((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \land x = W ++ ⟨“ v ”⟩) \to x prefix \|W\| = W$
36	35	eqcomd	$⊢ (((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \land x = W ++ ⟨“ v ”⟩) \to W = x prefix \|W\|$
37	36	ex	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to (x = W ++ ⟨“ v ”⟩ \to W = x prefix \|W\|)$
38	28 37	impbid	$⊢ ((((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \land x \in X) \to (W = x prefix \|W\| \leftrightarrow x = W ++ ⟨“ v ”⟩)$
39	38	ralrimiva	$⊢ (((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \to \forall x \in X (W = x prefix \|W\| \leftrightarrow x = W ++ ⟨“ v ”⟩)$
40		reu6i	$⊢ (W ++ ⟨“ v ”⟩ \in X \land \forall x \in X (W = x prefix \|W\| \leftrightarrow x = W ++ ⟨“ v ”⟩)) \to \exists! x \in X W = x prefix \|W\|$
41	21 39 40	syl2anc	$⊢ (((W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \land v \in V) \land (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u))) \to \exists! x \in X W = x prefix \|W\|$
42	41	exp31	$⊢ (W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \to (v \in V \to ((W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u)) \to \exists! x \in X W = x prefix \|W\|))$
43	18 20 42	rexlimd	$⊢ (W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \to (\exists v \in V (W ++ ⟨“ v ”⟩ \in X \land \forall u \in V (W ++ ⟨“ u ”⟩ \in X \to v = u)) \to \exists! x \in X W = x prefix \|W\|)$
44	14 43	biimtrid	$⊢ (W \in Word V \land \forall y \in X (y \in Word V \land \|y\| = \|W\| + 1)) \to (\exists! v \in V W ++ ⟨“ v ”⟩ \in X \to \exists! x \in X W = x prefix \|W\|)$
45	5 44	sylan2b	$⊢ (W \in Word V \land \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1)) \to (\exists! v \in V W ++ ⟨“ v ”⟩ \in X \to \exists! x \in X W = x prefix \|W\|)$

Metamath Proof Explorer

Theorem reuccatpfxs1

Proof