reuccatpfxs1lem

		Ref	Expression
	Assertion	reuccatpfxs1lem	$⊢ ((W \in Word V \land U \in X) \land \forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \land \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1)) \to (W = U prefix \|W\| \to U = W ++ ⟨“ S ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = U \to (x \in Word V \leftrightarrow U \in Word V)$
2		fveqeq2	$⊢ x = U \to (\|x\| = \|W\| + 1 \leftrightarrow \|U\| = \|W\| + 1)$
3	1 2	anbi12d	$⊢ x = U \to ((x \in Word V \land \|x\| = \|W\| + 1) \leftrightarrow (U \in Word V \land \|U\| = \|W\| + 1))$
4	3	rspcv	$⊢ U \in X \to (\forall x \in X (x \in Word V \land \|x\| = \|W\| + 1) \to (U \in Word V \land \|U\| = \|W\| + 1))$
5	4	adantl	$⊢ (W \in Word V \land U \in X) \to (\forall x \in X (x \in Word V \land \|x\| = \|W\| + 1) \to (U \in Word V \land \|U\| = \|W\| + 1))$
6		simpl	$⊢ (W \in Word V \land U \in X) \to W \in Word V$
7	6	adantr	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to W \in Word V$
8		simpl	$⊢ (U \in Word V \land \|U\| = \|W\| + 1) \to U \in Word V$
9	8	adantl	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to U \in Word V$
10		simprr	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to \|U\| = \|W\| + 1$
11		ccats1pfxeqrex	$⊢ (W \in Word V \land U \in Word V \land \|U\| = \|W\| + 1) \to (W = U prefix \|W\| \to \exists u \in V U = W ++ ⟨“ u ”⟩)$
12	7 9 10 11	syl3anc	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to (W = U prefix \|W\| \to \exists u \in V U = W ++ ⟨“ u ”⟩)$
13		s1eq	$⊢ s = u \to ⟨“ s ”⟩ = ⟨“ u ”⟩$
14	13	oveq2d	$⊢ s = u \to W ++ ⟨“ s ”⟩ = W ++ ⟨“ u ”⟩$
15	14	eleq1d	$⊢ s = u \to (W ++ ⟨“ s ”⟩ \in X \leftrightarrow W ++ ⟨“ u ”⟩ \in X)$
16		eqeq2	$⊢ s = u \to (S = s \leftrightarrow S = u)$
17	15 16	imbi12d	$⊢ s = u \to ((W ++ ⟨“ s ”⟩ \in X \to S = s) \leftrightarrow (W ++ ⟨“ u ”⟩ \in X \to S = u))$
18	17	rspcv	$⊢ u \in V \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to (W ++ ⟨“ u ”⟩ \in X \to S = u))$
19		eleq1	$⊢ U = W ++ ⟨“ u ”⟩ \to (U \in X \leftrightarrow W ++ ⟨“ u ”⟩ \in X)$
20		id	$⊢ (W ++ ⟨“ u ”⟩ \in X \to S = u) \to (W ++ ⟨“ u ”⟩ \in X \to S = u)$
21	20	imp	$⊢ ((W ++ ⟨“ u ”⟩ \in X \to S = u) \land W ++ ⟨“ u ”⟩ \in X) \to S = u$
22	21	eqcomd	$⊢ ((W ++ ⟨“ u ”⟩ \in X \to S = u) \land W ++ ⟨“ u ”⟩ \in X) \to u = S$
23	22	s1eqd	$⊢ ((W ++ ⟨“ u ”⟩ \in X \to S = u) \land W ++ ⟨“ u ”⟩ \in X) \to ⟨“ u ”⟩ = ⟨“ S ”⟩$
24	23	oveq2d	$⊢ ((W ++ ⟨“ u ”⟩ \in X \to S = u) \land W ++ ⟨“ u ”⟩ \in X) \to W ++ ⟨“ u ”⟩ = W ++ ⟨“ S ”⟩$
25	24	eqeq2d	$⊢ ((W ++ ⟨“ u ”⟩ \in X \to S = u) \land W ++ ⟨“ u ”⟩ \in X) \to (U = W ++ ⟨“ u ”⟩ \leftrightarrow U = W ++ ⟨“ S ”⟩)$
26	25	biimpd	$⊢ ((W ++ ⟨“ u ”⟩ \in X \to S = u) \land W ++ ⟨“ u ”⟩ \in X) \to (U = W ++ ⟨“ u ”⟩ \to U = W ++ ⟨“ S ”⟩)$
27	26	ex	$⊢ (W ++ ⟨“ u ”⟩ \in X \to S = u) \to (W ++ ⟨“ u ”⟩ \in X \to (U = W ++ ⟨“ u ”⟩ \to U = W ++ ⟨“ S ”⟩))$
28	27	com13	$⊢ U = W ++ ⟨“ u ”⟩ \to (W ++ ⟨“ u ”⟩ \in X \to ((W ++ ⟨“ u ”⟩ \in X \to S = u) \to U = W ++ ⟨“ S ”⟩))$
29	19 28	sylbid	$⊢ U = W ++ ⟨“ u ”⟩ \to (U \in X \to ((W ++ ⟨“ u ”⟩ \in X \to S = u) \to U = W ++ ⟨“ S ”⟩))$
30	29	com3l	$⊢ U \in X \to ((W ++ ⟨“ u ”⟩ \in X \to S = u) \to (U = W ++ ⟨“ u ”⟩ \to U = W ++ ⟨“ S ”⟩))$
31	18 30	sylan9r	$⊢ (U \in X \land u \in V) \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to (U = W ++ ⟨“ u ”⟩ \to U = W ++ ⟨“ S ”⟩))$
32	31	com23	$⊢ (U \in X \land u \in V) \to (U = W ++ ⟨“ u ”⟩ \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to U = W ++ ⟨“ S ”⟩))$
33	32	rexlimdva	$⊢ U \in X \to (\exists u \in V U = W ++ ⟨“ u ”⟩ \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to U = W ++ ⟨“ S ”⟩))$
34	33	adantl	$⊢ (W \in Word V \land U \in X) \to (\exists u \in V U = W ++ ⟨“ u ”⟩ \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to U = W ++ ⟨“ S ”⟩))$
35	34	adantr	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to (\exists u \in V U = W ++ ⟨“ u ”⟩ \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to U = W ++ ⟨“ S ”⟩))$
36	12 35	syld	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to (W = U prefix \|W\| \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to U = W ++ ⟨“ S ”⟩))$
37	36	com23	$⊢ ((W \in Word V \land U \in X) \land (U \in Word V \land \|U\| = \|W\| + 1)) \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to (W = U prefix \|W\| \to U = W ++ ⟨“ S ”⟩))$
38	37	ex	$⊢ (W \in Word V \land U \in X) \to ((U \in Word V \land \|U\| = \|W\| + 1) \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to (W = U prefix \|W\| \to U = W ++ ⟨“ S ”⟩)))$
39	5 38	syld	$⊢ (W \in Word V \land U \in X) \to (\forall x \in X (x \in Word V \land \|x\| = \|W\| + 1) \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to (W = U prefix \|W\| \to U = W ++ ⟨“ S ”⟩)))$
40	39	com23	$⊢ (W \in Word V \land U \in X) \to (\forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \to (\forall x \in X (x \in Word V \land \|x\| = \|W\| + 1) \to (W = U prefix \|W\| \to U = W ++ ⟨“ S ”⟩)))$
41	40	3imp	$⊢ ((W \in Word V \land U \in X) \land \forall s \in V (W ++ ⟨“ s ”⟩ \in X \to S = s) \land \forall x \in X (x \in Word V \land \|x\| = \|W\| + 1)) \to (W = U prefix \|W\| \to U = W ++ ⟨“ S ”⟩)$

Metamath Proof Explorer

Theorem reuccatpfxs1lem

Proof