wrd2ind

Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019) (Proof shortened by AV, 12-Oct-2022)

	Ref	Expression
Hypotheses	wrd2ind.1	$⊢ (x = \emptyset \land w = \emptyset) \to (φ \leftrightarrow ψ)$
	wrd2ind.2	$⊢ (x = y \land w = u) \to (φ \leftrightarrow χ)$
	wrd2ind.3	$⊢ (x = y ++ ⟨“ z ”⟩ \land w = u ++ ⟨“ s ”⟩) \to (φ \leftrightarrow θ)$
	wrd2ind.4	$⊢ x = A \to (ρ \leftrightarrow τ)$
	wrd2ind.5	$⊢ w = B \to (φ \leftrightarrow ρ)$
	wrd2ind.6	$⊢ ψ$
	wrd2ind.7	$⊢ ((y \in Word X \land z \in X) \land (u \in Word Y \land s \in Y) \land \|y\| = \|u\|) \to (χ \to θ)$
Assertion	wrd2ind	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to τ$

Proof

Step	Hyp	Ref	Expression
1		wrd2ind.1	$⊢ (x = \emptyset \land w = \emptyset) \to (φ \leftrightarrow ψ)$
2		wrd2ind.2	$⊢ (x = y \land w = u) \to (φ \leftrightarrow χ)$
3		wrd2ind.3	$⊢ (x = y ++ ⟨“ z ”⟩ \land w = u ++ ⟨“ s ”⟩) \to (φ \leftrightarrow θ)$
4		wrd2ind.4	$⊢ x = A \to (ρ \leftrightarrow τ)$
5		wrd2ind.5	$⊢ w = B \to (φ \leftrightarrow ρ)$
6		wrd2ind.6	$⊢ ψ$
7		wrd2ind.7	$⊢ ((y \in Word X \land z \in X) \land (u \in Word Y \land s \in Y) \land \|y\| = \|u\|) \to (χ \to θ)$
8		lencl	$⊢ A \in Word X \to \|A\| \in ℕ_{0}$
9		eqeq2	$⊢ n = 0 \to (\|x\| = n \leftrightarrow \|x\| = 0)$
10	9	anbi2d	$⊢ n = 0 \to ((\|x\| = \|w\| \land \|x\| = n) \leftrightarrow (\|x\| = \|w\| \land \|x\| = 0))$
11	10	imbi1d	$⊢ n = 0 \to (((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow ((\|x\| = \|w\| \land \|x\| = 0) \to φ))$
12	11	2ralbidv	$⊢ n = 0 \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = 0) \to φ))$
13		eqeq2	$⊢ n = m \to (\|x\| = n \leftrightarrow \|x\| = m)$
14	13	anbi2d	$⊢ n = m \to ((\|x\| = \|w\| \land \|x\| = n) \leftrightarrow (\|x\| = \|w\| \land \|x\| = m))$
15	14	imbi1d	$⊢ n = m \to (((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow ((\|x\| = \|w\| \land \|x\| = m) \to φ))$
16	15	2ralbidv	$⊢ n = m \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m) \to φ))$
17		eqeq2	$⊢ n = m + 1 \to (\|x\| = n \leftrightarrow \|x\| = m + 1)$
18	17	anbi2d	$⊢ n = m + 1 \to ((\|x\| = \|w\| \land \|x\| = n) \leftrightarrow (\|x\| = \|w\| \land \|x\| = m + 1))$
19	18	imbi1d	$⊢ n = m + 1 \to (((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow ((\|x\| = \|w\| \land \|x\| = m + 1) \to φ))$
20	19	2ralbidv	$⊢ n = m + 1 \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m + 1) \to φ))$
21		eqeq2	$⊢ n = \|A\| \to (\|x\| = n \leftrightarrow \|x\| = \|A\|)$
22	21	anbi2d	$⊢ n = \|A\| \to ((\|x\| = \|w\| \land \|x\| = n) \leftrightarrow (\|x\| = \|w\| \land \|x\| = \|A\|))$
23	22	imbi1d	$⊢ n = \|A\| \to (((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ))$
24	23	2ralbidv	$⊢ n = \|A\| \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = n) \to φ) \leftrightarrow \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ))$
25		eqeq1	$⊢ \|x\| = 0 \to (\|x\| = \|w\| \leftrightarrow 0 = \|w\|)$
26	25	adantl	$⊢ ((w \in Word Y \land x \in Word X) \land \|x\| = 0) \to (\|x\| = \|w\| \leftrightarrow 0 = \|w\|)$
27		eqcom	$⊢ 0 = \|w\| \leftrightarrow \|w\| = 0$
28		hasheq0	$⊢ w \in Word Y \to (\|w\| = 0 \leftrightarrow w = \emptyset)$
29	27 28	bitrid	$⊢ w \in Word Y \to (0 = \|w\| \leftrightarrow w = \emptyset)$
30		hasheq0	$⊢ x \in Word X \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
31	6 1	mpbiri	$⊢ (x = \emptyset \land w = \emptyset) \to φ$
32	31	ex	$⊢ x = \emptyset \to (w = \emptyset \to φ)$
33	30 32	syl6bi	$⊢ x \in Word X \to (\|x\| = 0 \to (w = \emptyset \to φ))$
34	33	com13	$⊢ w = \emptyset \to (\|x\| = 0 \to (x \in Word X \to φ))$
35	29 34	syl6bi	$⊢ w \in Word Y \to (0 = \|w\| \to (\|x\| = 0 \to (x \in Word X \to φ)))$
36	35	com24	$⊢ w \in Word Y \to (x \in Word X \to (\|x\| = 0 \to (0 = \|w\| \to φ)))$
37	36	imp31	$⊢ ((w \in Word Y \land x \in Word X) \land \|x\| = 0) \to (0 = \|w\| \to φ)$
38	26 37	sylbid	$⊢ ((w \in Word Y \land x \in Word X) \land \|x\| = 0) \to (\|x\| = \|w\| \to φ)$
39	38	ex	$⊢ (w \in Word Y \land x \in Word X) \to (\|x\| = 0 \to (\|x\| = \|w\| \to φ))$
40	39	impcomd	$⊢ (w \in Word Y \land x \in Word X) \to ((\|x\| = \|w\| \land \|x\| = 0) \to φ)$
41	40	rgen2	$⊢ \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = 0) \to φ)$
42		fveq2	$⊢ x = y \to \|x\| = \|y\|$
43		fveq2	$⊢ w = u \to \|w\| = \|u\|$
44	42 43	eqeqan12d	$⊢ (x = y \land w = u) \to (\|x\| = \|w\| \leftrightarrow \|y\| = \|u\|)$
45		fveqeq2	$⊢ x = y \to (\|x\| = m \leftrightarrow \|y\| = m)$
46	45	adantr	$⊢ (x = y \land w = u) \to (\|x\| = m \leftrightarrow \|y\| = m)$
47	44 46	anbi12d	$⊢ (x = y \land w = u) \to ((\|x\| = \|w\| \land \|x\| = m) \leftrightarrow (\|y\| = \|u\| \land \|y\| = m))$
48	47 2	imbi12d	$⊢ (x = y \land w = u) \to (((\|x\| = \|w\| \land \|x\| = m) \to φ) \leftrightarrow ((\|y\| = \|u\| \land \|y\| = m) \to χ))$
49	48	ancoms	$⊢ (w = u \land x = y) \to (((\|x\| = \|w\| \land \|x\| = m) \to φ) \leftrightarrow ((\|y\| = \|u\| \land \|y\| = m) \to χ))$
50	49	cbvraldva	$⊢ w = u \to (\forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m) \to φ) \leftrightarrow \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ))$
51	50	cbvralvw	$⊢ \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m) \to φ) \leftrightarrow \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)$
52		pfxcl	$⊢ w \in Word Y \to w prefix (\|w\| - 1) \in Word Y$
53	52	adantr	$⊢ (w \in Word Y \land x \in Word X) \to w prefix (\|w\| - 1) \in Word Y$
54	53	ad2antrl	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w prefix (\|w\| - 1) \in Word Y$
55		simprll	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w \in Word Y$
56		eqeq1	$⊢ \|x\| = m + 1 \to (\|x\| = \|w\| \leftrightarrow m + 1 = \|w\|)$
57		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
58		eleq1	$⊢ \|w\| = m + 1 \to (\|w\| \in ℕ \leftrightarrow m + 1 \in ℕ)$
59	58	eqcoms	$⊢ m + 1 = \|w\| \to (\|w\| \in ℕ \leftrightarrow m + 1 \in ℕ)$
60	57 59	imbitrrid	$⊢ m + 1 = \|w\| \to (m \in ℕ_{0} \to \|w\| \in ℕ)$
61	56 60	syl6bi	$⊢ \|x\| = m + 1 \to (\|x\| = \|w\| \to (m \in ℕ_{0} \to \|w\| \in ℕ))$
62	61	impcom	$⊢ (\|x\| = \|w\| \land \|x\| = m + 1) \to (m \in ℕ_{0} \to \|w\| \in ℕ)$
63	62	adantl	$⊢ ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1)) \to (m \in ℕ_{0} \to \|w\| \in ℕ)$
64	63	impcom	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|w\| \in ℕ$
65	64	nnge1d	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to 1 \leq \|w\|$
66		wrdlenge1n0	$⊢ w \in Word Y \to (w \neq \emptyset \leftrightarrow 1 \leq \|w\|)$
67	55 66	syl	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (w \neq \emptyset \leftrightarrow 1 \leq \|w\|)$
68	65 67	mpbird	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w \neq \emptyset$
69		lswcl	$⊢ (w \in Word Y \land w \neq \emptyset) \to lastS (w) \in Y$
70	55 68 69	syl2anc	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to lastS (w) \in Y$
71	54 70	jca	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (w prefix (\|w\| - 1) \in Word Y \land lastS (w) \in Y)$
72		pfxcl	$⊢ x \in Word X \to x prefix (\|x\| - 1) \in Word X$
73	72	adantl	$⊢ (w \in Word Y \land x \in Word X) \to x prefix (\|x\| - 1) \in Word X$
74	73	ad2antrl	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x prefix (\|x\| - 1) \in Word X$
75		simprlr	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x \in Word X$
76		eleq1	$⊢ \|x\| = m + 1 \to (\|x\| \in ℕ \leftrightarrow m + 1 \in ℕ)$
77	57 76	imbitrrid	$⊢ \|x\| = m + 1 \to (m \in ℕ_{0} \to \|x\| \in ℕ)$
78	77	ad2antll	$⊢ ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1)) \to (m \in ℕ_{0} \to \|x\| \in ℕ)$
79	78	impcom	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| \in ℕ$
80	79	nnge1d	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to 1 \leq \|x\|$
81		wrdlenge1n0	$⊢ x \in Word X \to (x \neq \emptyset \leftrightarrow 1 \leq \|x\|)$
82	75 81	syl	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (x \neq \emptyset \leftrightarrow 1 \leq \|x\|)$
83	80 82	mpbird	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x \neq \emptyset$
84		lswcl	$⊢ (x \in Word X \land x \neq \emptyset) \to lastS (x) \in X$
85	75 83 84	syl2anc	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to lastS (x) \in X$
86	71 74 85	jca32	$⊢ (m \in ℕ_{0} \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to ((w prefix (\|w\| - 1) \in Word Y \land lastS (w) \in Y) \land (x prefix (\|x\| - 1) \in Word X \land lastS (x) \in X))$
87	86	adantlr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to ((w prefix (\|w\| - 1) \in Word Y \land lastS (w) \in Y) \land (x prefix (\|x\| - 1) \in Word X \land lastS (x) \in X))$
88		simprl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (w \in Word Y \land x \in Word X)$
89		simplr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)$
90		simprrl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| = \|w\|$
91	90	oveq1d	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| - 1 = \|w\| - 1$
92		simprlr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x \in Word X$
93		fzossfz	$⊢ (0 ..^\|x\|) \subseteq (0 \dots \|x\|)$
94		simprrr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| = m + 1$
95	57	ad2antrr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to m + 1 \in ℕ$
96	94 95	eqeltrd	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| \in ℕ$
97		fzo0end	$⊢ \|x\| \in ℕ \to \|x\| - 1 \in (0 ..^\|x\|)$
98	96 97	syl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| - 1 \in (0 ..^\|x\|)$
99	93 98	sselid	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| - 1 \in (0 \dots \|x\|)$
100		pfxlen	$⊢ (x \in Word X \land \|x\| - 1 \in (0 \dots \|x\|)) \to \|x prefix (\|x\| - 1)\| = \|x\| - 1$
101	92 99 100	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x prefix (\|x\| - 1)\| = \|x\| - 1$
102		simprll	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w \in Word Y$
103		oveq1	$⊢ \|w\| = \|x\| \to \|w\| - 1 = \|x\| - 1$
104		oveq2	$⊢ \|w\| = \|x\| \to (0 \dots \|w\|) = (0 \dots \|x\|)$
105	103 104	eleq12d	$⊢ \|w\| = \|x\| \to (\|w\| - 1 \in (0 \dots \|w\|) \leftrightarrow \|x\| - 1 \in (0 \dots \|x\|))$
106	105	eqcoms	$⊢ \|x\| = \|w\| \to (\|w\| - 1 \in (0 \dots \|w\|) \leftrightarrow \|x\| - 1 \in (0 \dots \|x\|))$
107	106	adantr	$⊢ (\|x\| = \|w\| \land \|x\| = m + 1) \to (\|w\| - 1 \in (0 \dots \|w\|) \leftrightarrow \|x\| - 1 \in (0 \dots \|x\|))$
108	107	ad2antll	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (\|w\| - 1 \in (0 \dots \|w\|) \leftrightarrow \|x\| - 1 \in (0 \dots \|x\|))$
109	99 108	mpbird	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|w\| - 1 \in (0 \dots \|w\|)$
110		pfxlen	$⊢ (w \in Word Y \land \|w\| - 1 \in (0 \dots \|w\|)) \to \|w prefix (\|w\| - 1)\| = \|w\| - 1$
111	102 109 110	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|w prefix (\|w\| - 1)\| = \|w\| - 1$
112	91 101 111	3eqtr4d	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|$
113	94	oveq1d	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x\| - 1 = m + 1 - 1$
114		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
115	114	ad2antrr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to m \in ℂ$
116		ax-1cn	$⊢ 1 \in ℂ$
117		pncan	$⊢ (m \in ℂ \land 1 \in ℂ) \to m + 1 - 1 = m$
118	115 116 117	sylancl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to m + 1 - 1 = m$
119	101 113 118	3eqtrd	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|x prefix (\|x\| - 1)\| = m$
120	112 119	jca	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (\|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\| \land \|x prefix (\|x\| - 1)\| = m)$
121	73	adantr	$⊢ ((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \to x prefix (\|x\| - 1) \in Word X$
122		fveq2	$⊢ y = x prefix (\|x\| - 1) \to \|y\| = \|x prefix (\|x\| - 1)\|$
123		fveq2	$⊢ u = w prefix (\|w\| - 1) \to \|u\| = \|w prefix (\|w\| - 1)\|$
124	122 123	eqeqan12d	$⊢ (y = x prefix (\|x\| - 1) \land u = w prefix (\|w\| - 1)) \to (\|y\| = \|u\| \leftrightarrow \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|)$
125	124	expcom	$⊢ u = w prefix (\|w\| - 1) \to (y = x prefix (\|x\| - 1) \to (\|y\| = \|u\| \leftrightarrow \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|))$
126	125	adantl	$⊢ ((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \to (y = x prefix (\|x\| - 1) \to (\|y\| = \|u\| \leftrightarrow \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|))$
127	126	imp	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (\|y\| = \|u\| \leftrightarrow \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|)$
128		fveqeq2	$⊢ y = x prefix (\|x\| - 1) \to (\|y\| = m \leftrightarrow \|x prefix (\|x\| - 1)\| = m)$
129	128	adantl	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (\|y\| = m \leftrightarrow \|x prefix (\|x\| - 1)\| = m)$
130	127 129	anbi12d	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to ((\|y\| = \|u\| \land \|y\| = m) \leftrightarrow (\|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\| \land \|x prefix (\|x\| - 1)\| = m))$
131		vex	$⊢ y \in V$
132		vex	$⊢ u \in V$
133	131 132 2	sbc2ie	$⊢ \underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ \leftrightarrow χ$
134	133	bicomi	$⊢ χ \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ$
135	134	a1i	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (χ \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ)$
136		simpr	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to y = x prefix (\|x\| - 1)$
137	136	sbceq1d	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ)$
138		dfsbcq	$⊢ u = w prefix (\|w\| - 1) \to (\underset{˙}{[} u / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
139	138	sbcbidv	$⊢ u = w prefix (\|w\| - 1) \to (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
140	139	adantl	$⊢ ((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \to (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
141	140	adantr	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} u / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
142	135 137 141	3bitrd	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (χ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
143	130 142	imbi12d	$⊢ (((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \land y = x prefix (\|x\| - 1)) \to (((\|y\| = \|u\| \land \|y\| = m) \to χ) \leftrightarrow ((\|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\| \land \|x prefix (\|x\| - 1)\| = m) \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ))$
144	121 143	rspcdv	$⊢ ((w \in Word Y \land x \in Word X) \land u = w prefix (\|w\| - 1)) \to (\forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ) \to ((\|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\| \land \|x prefix (\|x\| - 1)\| = m) \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ))$
145	53 144	rspcimdv	$⊢ (w \in Word Y \land x \in Word X) \to (\forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ) \to ((\|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\| \land \|x prefix (\|x\| - 1)\| = m) \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ))$
146	88 89 120 145	syl3c	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ$
147	146 112	jca	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|)$
148		dfsbcq	$⊢ u = w prefix (\|w\| - 1) \to (\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ)$
149		sbccom	$⊢ \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ$
150	148 149	bitrdi	$⊢ u = w prefix (\|w\| - 1) \to (\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
151	123	eqeq2d	$⊢ u = w prefix (\|w\| - 1) \to (\|y\| = \|u\| \leftrightarrow \|y\| = \|w prefix (\|w\| - 1)\|)$
152	150 151	anbi12d	$⊢ u = w prefix (\|w\| - 1) \to ((\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \land \|y\| = \|u\|) \leftrightarrow (\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|))$
153		oveq1	$⊢ u = w prefix (\|w\| - 1) \to u ++ ⟨“ s ”⟩ = (w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩$
154	153	sbceq1d	$⊢ u = w prefix (\|w\| - 1) \to (\underset{˙}{[} (u ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ)$
155	152 154	imbi12d	$⊢ u = w prefix (\|w\| - 1) \to (((\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \land \|y\| = \|u\|) \to \underset{˙}{[} (u ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ) \leftrightarrow ((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ))$
156		s1eq	$⊢ s = lastS (w) \to ⟨“ s ”⟩ = ⟨“ lastS (w) ”⟩$
157	156	oveq2d	$⊢ s = lastS (w) \to (w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩ = (w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩$
158	157	sbceq1d	$⊢ s = lastS (w) \to (\underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ)$
159	158	imbi2d	$⊢ s = lastS (w) \to (((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ) \leftrightarrow ((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ))$
160		sbccom	$⊢ \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ$
161	160	a1i	$⊢ s = lastS (w) \to (\underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
162	161	imbi2d	$⊢ s = lastS (w) \to (((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ) \leftrightarrow ((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ))$
163	159 162	bitrd	$⊢ s = lastS (w) \to (((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ) \leftrightarrow ((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ))$
164		dfsbcq	$⊢ y = x prefix (\|x\| - 1) \to (\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ)$
165		fveqeq2	$⊢ y = x prefix (\|x\| - 1) \to (\|y\| = \|w prefix (\|w\| - 1)\| \leftrightarrow \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|)$
166	164 165	anbi12d	$⊢ y = x prefix (\|x\| - 1) \to ((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \leftrightarrow (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|))$
167		oveq1	$⊢ y = x prefix (\|x\| - 1) \to y ++ ⟨“ z ”⟩ = (x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩$
168	167	sbceq1d	$⊢ y = x prefix (\|x\| - 1) \to (\underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
169	166 168	imbi12d	$⊢ y = x prefix (\|x\| - 1) \to (((\underset{˙}{[} y / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|y\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ) \leftrightarrow ((\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ))$
170		s1eq	$⊢ z = lastS (x) \to ⟨“ z ”⟩ = ⟨“ lastS (x) ”⟩$
171	170	oveq2d	$⊢ z = lastS (x) \to (x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩ = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩$
172	171	sbceq1d	$⊢ z = lastS (x) \to (\underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
173	172	imbi2d	$⊢ z = lastS (x) \to (((\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ) \leftrightarrow ((\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ))$
174		simplr	$⊢ (((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \land \|y\| = \|u\|) \to (y \in Word X \land z \in X)$
175		simpll	$⊢ (((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \land \|y\| = \|u\|) \to (u \in Word Y \land s \in Y)$
176		simpr	$⊢ (((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \land \|y\| = \|u\|) \to \|y\| = \|u\|$
177	174 175 176 7	syl3anc	$⊢ (((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \land \|y\| = \|u\|) \to (χ \to θ)$
178	2	ancoms	$⊢ (w = u \land x = y) \to (φ \leftrightarrow χ)$
179	132 131 178	sbc2ie	$⊢ \underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow χ$
180		ovex	$⊢ u ++ ⟨“ s ”⟩ \in V$
181		ovex	$⊢ y ++ ⟨“ z ”⟩ \in V$
182	3	ancoms	$⊢ (w = u ++ ⟨“ s ”⟩ \land x = y ++ ⟨“ z ”⟩) \to (φ \leftrightarrow θ)$
183	180 181 182	sbc2ie	$⊢ \underset{˙}{[} (u ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow θ$
184	177 179 183	3imtr4g	$⊢ (((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \land \|y\| = \|u\|) \to (\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \to \underset{˙}{[} (u ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ)$
185	184	ex	$⊢ ((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \to (\|y\| = \|u\| \to (\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \to \underset{˙}{[} (u ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ))$
186	185	impcomd	$⊢ ((u \in Word Y \land s \in Y) \land (y \in Word X \land z \in X)) \to ((\underset{˙}{[} u / w \underset{˙}{]} \underset{˙}{[} y / x \underset{˙}{]} φ \land \|y\| = \|u\|) \to \underset{˙}{[} (u ++ ⟨“ s ”⟩) / w \underset{˙}{]} \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ)$
187	155 163 169 173 186	vtocl4ga	$⊢ ((w prefix (\|w\| - 1) \in Word Y \land lastS (w) \in Y) \land (x prefix (\|x\| - 1) \in Word X \land lastS (x) \in X)) \to ((\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} \underset{˙}{[} (w prefix (\|w\| - 1)) / w \underset{˙}{]} φ \land \|x prefix (\|x\| - 1)\| = \|w prefix (\|w\| - 1)\|) \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
188	87 147 187	sylc	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ$
189		eqtr2	$⊢ (\|x\| = \|w\| \land \|x\| = m + 1) \to \|w\| = m + 1$
190	189	ad2antll	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|w\| = m + 1$
191	190 95	eqeltrd	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to \|w\| \in ℕ$
192		wrdfin	$⊢ w \in Word Y \to w \in Fin$
193	192	adantr	$⊢ (w \in Word Y \land x \in Word X) \to w \in Fin$
194	193	ad2antrl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w \in Fin$
195		hashnncl	$⊢ w \in Fin \to (\|w\| \in ℕ \leftrightarrow w \neq \emptyset)$
196	194 195	syl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (\|w\| \in ℕ \leftrightarrow w \neq \emptyset)$
197	191 196	mpbid	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w \neq \emptyset$
198		pfxlswccat	$⊢ (w \in Word Y \land w \neq \emptyset) \to (w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩ = w$
199	198	eqcomd	$⊢ (w \in Word Y \land w \neq \emptyset) \to w = (w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩$
200	102 197 199	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to w = (w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩$
201		wrdfin	$⊢ x \in Word X \to x \in Fin$
202	201	adantl	$⊢ (w \in Word Y \land x \in Word X) \to x \in Fin$
203	202	ad2antrl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x \in Fin$
204		hashnncl	$⊢ x \in Fin \to (\|x\| \in ℕ \leftrightarrow x \neq \emptyset)$
205	203 204	syl	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (\|x\| \in ℕ \leftrightarrow x \neq \emptyset)$
206	96 205	mpbid	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x \neq \emptyset$
207		pfxlswccat	$⊢ (x \in Word X \land x \neq \emptyset) \to (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩ = x$
208	207	eqcomd	$⊢ (x \in Word X \land x \neq \emptyset) \to x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩$
209	92 206 208	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩$
210		sbceq1a	$⊢ w = (w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩ \to (φ \leftrightarrow \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
211		sbceq1a	$⊢ x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩ \to (\underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
212	210 211	sylan9bb	$⊢ (w = (w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩ \land x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) \to (φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
213	200 209 212	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to (φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} \underset{˙}{[} ((w prefix (\|w\| - 1)) ++ ⟨“ lastS (w) ”⟩) / w \underset{˙}{]} φ)$
214	188 213	mpbird	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land ((w \in Word Y \land x \in Word X) \land (\|x\| = \|w\| \land \|x\| = m + 1))) \to φ$
215	214	expr	$⊢ ((m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \land (w \in Word Y \land x \in Word X)) \to ((\|x\| = \|w\| \land \|x\| = m + 1) \to φ)$
216	215	ralrimivva	$⊢ (m \in ℕ_{0} \land \forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ)) \to \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m + 1) \to φ)$
217	216	ex	$⊢ m \in ℕ_{0} \to (\forall u \in Word Y \forall y \in Word X ((\|y\| = \|u\| \land \|y\| = m) \to χ) \to \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m + 1) \to φ))$
218	51 217	biimtrid	$⊢ m \in ℕ_{0} \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m) \to φ) \to \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = m + 1) \to φ))$
219	12 16 20 24 41 218	nn0ind	$⊢ \|A\| \in ℕ_{0} \to \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ)$
220	8 219	syl	$⊢ A \in Word X \to \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ)$
221	220	3ad2ant1	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to \forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ)$
222		fveq2	$⊢ w = B \to \|w\| = \|B\|$
223	222	eqeq2d	$⊢ w = B \to (\|x\| = \|w\| \leftrightarrow \|x\| = \|B\|)$
224	223	anbi1d	$⊢ w = B \to ((\|x\| = \|w\| \land \|x\| = \|A\|) \leftrightarrow (\|x\| = \|B\| \land \|x\| = \|A\|))$
225	224 5	imbi12d	$⊢ w = B \to (((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ) \leftrightarrow ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ))$
226	225	ralbidv	$⊢ w = B \to (\forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ) \leftrightarrow \forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ))$
227	226	rspcv	$⊢ B \in Word Y \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ) \to \forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ))$
228	227	3ad2ant2	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to (\forall w \in Word Y \forall x \in Word X ((\|x\| = \|w\| \land \|x\| = \|A\|) \to φ) \to \forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ))$
229	221 228	mpd	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to \forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ)$
230		eqidd	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to \|A\| = \|A\|$
231		fveqeq2	$⊢ x = A \to (\|x\| = \|B\| \leftrightarrow \|A\| = \|B\|)$
232		fveqeq2	$⊢ x = A \to (\|x\| = \|A\| \leftrightarrow \|A\| = \|A\|)$
233	231 232	anbi12d	$⊢ x = A \to ((\|x\| = \|B\| \land \|x\| = \|A\|) \leftrightarrow (\|A\| = \|B\| \land \|A\| = \|A\|))$
234	233 4	imbi12d	$⊢ x = A \to (((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \leftrightarrow ((\|A\| = \|B\| \land \|A\| = \|A\|) \to τ))$
235	234	rspcv	$⊢ A \in Word X \to (\forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \to ((\|A\| = \|B\| \land \|A\| = \|A\|) \to τ))$
236	235	com23	$⊢ A \in Word X \to ((\|A\| = \|B\| \land \|A\| = \|A\|) \to (\forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \to τ))$
237	236	expd	$⊢ A \in Word X \to (\|A\| = \|B\| \to (\|A\| = \|A\| \to (\forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \to τ)))$
238	237	com34	$⊢ A \in Word X \to (\|A\| = \|B\| \to (\forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \to (\|A\| = \|A\| \to τ)))$
239	238	imp	$⊢ (A \in Word X \land \|A\| = \|B\|) \to (\forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \to (\|A\| = \|A\| \to τ))$
240	239	3adant2	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to (\forall x \in Word X ((\|x\| = \|B\| \land \|x\| = \|A\|) \to ρ) \to (\|A\| = \|A\| \to τ))$
241	229 230 240	mp2d	$⊢ (A \in Word X \land B \in Word Y \land \|A\| = \|B\|) \to τ$

Metamath Proof Explorer

Theorem wrd2ind

Proof