chnerlem1

Description: In a chain constructed on an equivalence relation, the last element is equivalent to any. This theorem is a translation of chnub to equivalence relations. (Contributed by Ender Ting, 29-Jan-2026)

	Ref	Expression
Hypotheses	chner.1	$⊢ φ \to \underset{˙}{\sim} Er A$
	chner.2	$⊢ φ \to C \in {Chain}_{A} \underset{˙}{\sim}$
	chner.3	$⊢ φ \to J \in (0 ..^\|C\|)$
Assertion	chnerlem1	$⊢ φ \to C (J) \underset{˙}{\sim} lastS (C)$

Proof

Step	Hyp	Ref	Expression
1		chner.1	$⊢ φ \to \underset{˙}{\sim} Er A$
2		chner.2	$⊢ φ \to C \in {Chain}_{A} \underset{˙}{\sim}$
3		chner.3	$⊢ φ \to J \in (0 ..^\|C\|)$
4		fveq2	$⊢ i = J \to C (i) = C (J)$
5	4	breq1d	$⊢ i = J \to (C (i) \underset{˙}{\sim} lastS (C) \leftrightarrow C (J) \underset{˙}{\sim} lastS (C))$
6		fveq2	$⊢ c = \emptyset \to \|c\| = \|\emptyset\|$
7	6	oveq2d	$⊢ c = \emptyset \to (0 ..^\|c\|) = (0 ..^\|\emptyset\|)$
8		fveq1	$⊢ c = \emptyset \to c (i) = \emptyset (i)$
9		fveq2	$⊢ c = \emptyset \to lastS (c) = lastS (\emptyset)$
10	8 9	breq12d	$⊢ c = \emptyset \to (c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow \emptyset (i) \underset{˙}{\sim} lastS (\emptyset))$
11	7 10	raleqbidv	$⊢ c = \emptyset \to (\forall i \in (0 ..^\|c\|) c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow \forall i \in (0 ..^\|\emptyset\|) \emptyset (i) \underset{˙}{\sim} lastS (\emptyset))$
12		fveq2	$⊢ c = d \to \|c\| = \|d\|$
13	12	oveq2d	$⊢ c = d \to (0 ..^\|c\|) = (0 ..^\|d\|)$
14		fveq1	$⊢ c = d \to c (i) = d (i)$
15		fveq2	$⊢ c = d \to lastS (c) = lastS (d)$
16	14 15	breq12d	$⊢ c = d \to (c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow d (i) \underset{˙}{\sim} lastS (d))$
17	13 16	raleqbidv	$⊢ c = d \to (\forall i \in (0 ..^\|c\|) c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d))$
18		fveq2	$⊢ i = j \to c (i) = c (j)$
19	18	breq1d	$⊢ i = j \to (c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow c (j) \underset{˙}{\sim} lastS (c))$
20	19	cbvralvw	$⊢ \forall i \in (0 ..^\|c\|) c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow \forall j \in (0 ..^\|c\|) c (j) \underset{˙}{\sim} lastS (c)$
21		fveq2	$⊢ c = d ++ ⟨“ x ”⟩ \to \|c\| = \|d ++ ⟨“ x ”⟩\|$
22	21	oveq2d	$⊢ c = d ++ ⟨“ x ”⟩ \to (0 ..^\|c\|) = (0 ..^\|d ++ ⟨“ x ”⟩\|)$
23		fveq1	$⊢ c = d ++ ⟨“ x ”⟩ \to c (j) = (d ++ ⟨“ x ”⟩) (j)$
24		fveq2	$⊢ c = d ++ ⟨“ x ”⟩ \to lastS (c) = lastS (d ++ ⟨“ x ”⟩)$
25	23 24	breq12d	$⊢ c = d ++ ⟨“ x ”⟩ \to (c (j) \underset{˙}{\sim} lastS (c) \leftrightarrow (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩))$
26	22 25	raleqbidv	$⊢ c = d ++ ⟨“ x ”⟩ \to (\forall j \in (0 ..^\|c\|) c (j) \underset{˙}{\sim} lastS (c) \leftrightarrow \forall j \in (0 ..^\|d ++ ⟨“ x ”⟩\|) (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩))$
27	20 26	bitrid	$⊢ c = d ++ ⟨“ x ”⟩ \to (\forall i \in (0 ..^\|c\|) c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow \forall j \in (0 ..^\|d ++ ⟨“ x ”⟩\|) (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩))$
28		fveq2	$⊢ c = C \to \|c\| = \|C\|$
29	28	oveq2d	$⊢ c = C \to (0 ..^\|c\|) = (0 ..^\|C\|)$
30		fveq1	$⊢ c = C \to c (i) = C (i)$
31		fveq2	$⊢ c = C \to lastS (c) = lastS (C)$
32	30 31	breq12d	$⊢ c = C \to (c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow C (i) \underset{˙}{\sim} lastS (C))$
33	29 32	raleqbidv	$⊢ c = C \to (\forall i \in (0 ..^\|c\|) c (i) \underset{˙}{\sim} lastS (c) \leftrightarrow \forall i \in (0 ..^\|C\|) C (i) \underset{˙}{\sim} lastS (C))$
34		hash0	$⊢ \|\emptyset\| = 0$
35		0nnn	$⊢ \neg 0 \in ℕ$
36	34 35	eqneltri	$⊢ \neg \|\emptyset\| \in ℕ$
37		fzo0n0	$⊢ (0 ..^\|\emptyset\|) \neq \emptyset \leftrightarrow \|\emptyset\| \in ℕ$
38	36 37	mtbir	$⊢ \neg (0 ..^\|\emptyset\|) \neq \emptyset$
39		nne	$⊢ \neg (0 ..^\|\emptyset\|) \neq \emptyset \leftrightarrow (0 ..^\|\emptyset\|) = \emptyset$
40	38 39	mpbi	$⊢ (0 ..^\|\emptyset\|) = \emptyset$
41		rzal	$⊢ (0 ..^\|\emptyset\|) = \emptyset \to \forall i \in (0 ..^\|\emptyset\|) \emptyset (i) \underset{˙}{\sim} lastS (\emptyset)$
42	40 41	mp1i	$⊢ φ \to \forall i \in (0 ..^\|\emptyset\|) \emptyset (i) \underset{˙}{\sim} lastS (\emptyset)$
43	1	ad6antr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to \underset{˙}{\sim} Er A$
44		simp-5r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to x \in A$
45	43 44	erref	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to x \underset{˙}{\sim} x$
46		simp-6r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to d \in {Chain}_{A} \underset{˙}{\sim}$
47	46	chnwrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to d \in Word A$
48		simplr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)$
49		ccatws1len	$⊢ d \in Word A \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
50	47 49	syl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
51		fveq2	$⊢ d = \emptyset \to \|d\| = \|\emptyset\|$
52	51 34	eqtr2di	$⊢ d = \emptyset \to 0 = \|d\|$
53	52	eqcomd	$⊢ d = \emptyset \to \|d\| = 0$
54	53	adantl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to \|d\| = 0$
55	54	oveq1d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to \|d\| + 1 = 0 + 1$
56		0p1e1	$⊢ 0 + 1 = 1$
57	55 56	eqtrdi	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to \|d\| + 1 = 1$
58	50 57	eqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to \|d ++ ⟨“ x ”⟩\| = 1$
59	58	oveq2d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to (0 ..^\|d ++ ⟨“ x ”⟩\|) = (0 ..^1)$
60	48 59	eleqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to j \in (0 ..^1)$
61		fzo01	$⊢ (0 ..^1) = \{0\}$
62	60 61	eleqtrdi	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to j \in \{0\}$
63	62	elsnd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to j = 0$
64	52	adantl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to 0 = \|d\|$
65	63 64	eqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to j = \|d\|$
66		ccats1val2	$⊢ (d \in Word A \land x \in A \land j = \|d\|) \to (d ++ ⟨“ x ”⟩) (j) = x$
67	47 44 65 66	syl3anc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to (d ++ ⟨“ x ”⟩) (j) = x$
68		lswccats1	$⊢ (d \in Word A \land x \in A) \to lastS (d ++ ⟨“ x ”⟩) = x$
69	47 44 68	syl2anc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to lastS (d ++ ⟨“ x ”⟩) = x$
70	45 67 69	3brtr4d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d = \emptyset) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩)$
71	1	ad6antr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to \underset{˙}{\sim} Er A$
72		simp-6r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to d \in {Chain}_{A} \underset{˙}{\sim}$
73	72	chnwrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to d \in Word A$
74	73	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j = \|d\|) \to d \in Word A$
75		simp-6r	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j = \|d\|) \to x \in A$
76		simpr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j = \|d\|) \to j = \|d\|$
77	74 75 76 66	syl3anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j = \|d\|) \to (d ++ ⟨“ x ”⟩) (j) = x$
78		simp-4r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)$
79		neneq	$⊢ d \neq \emptyset \to \neg d = \emptyset$
80	79	adantl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to \neg d = \emptyset$
81	78 80	orcnd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to lastS (d) \underset{˙}{\sim} x$
82	71 81	ersym	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to x \underset{˙}{\sim} lastS (d)$
83	82	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j = \|d\|) \to x \underset{˙}{\sim} lastS (d)$
84	77 83	eqbrtrd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j = \|d\|) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d)$
85		fveq2	$⊢ i = j \to (d ++ ⟨“ x ”⟩) (i) = (d ++ ⟨“ x ”⟩) (j)$
86	85	breq1d	$⊢ i = j \to ((d ++ ⟨“ x ”⟩) (i) \underset{˙}{\sim} lastS (d) \leftrightarrow (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d))$
87		simp-4r	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)$
88		simplr	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to d \in {Chain}_{A} \underset{˙}{\sim}$
89	88	chnwrd	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to d \in Word A$
90		simpr	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to i \in (0 ..^\|d\|)$
91		ccats1val1	$⊢ (d \in Word A \land i \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (i) = d (i)$
92	89 90 91	syl2anc	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (i) = d (i)$
93	92	eqcomd	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to d (i) = (d ++ ⟨“ x ”⟩) (i)$
94	93	breq1d	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to (d (i) \underset{˙}{\sim} lastS (d) \leftrightarrow (d ++ ⟨“ x ”⟩) (i) \underset{˙}{\sim} lastS (d))$
95	94	ralbidva	$⊢ (φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \to (\forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d) \leftrightarrow \forall i \in (0 ..^\|d\|) (d ++ ⟨“ x ”⟩) (i) \underset{˙}{\sim} lastS (d))$
96	95	ad6antr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to (\forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d) \leftrightarrow \forall i \in (0 ..^\|d\|) (d ++ ⟨“ x ”⟩) (i) \underset{˙}{\sim} lastS (d))$
97	87 96	mpbid	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to \forall i \in (0 ..^\|d\|) (d ++ ⟨“ x ”⟩) (i) \underset{˙}{\sim} lastS (d)$
98		simpr	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)$
99		simp-5r	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to d \in {Chain}_{A} \underset{˙}{\sim}$
100	99	chnwrd	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to d \in Word A$
101	100 49	syl	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
102	101	oveq2d	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to (0 ..^\|d ++ ⟨“ x ”⟩\|) = (0 ..^\|d\| + 1)$
103	98 102	eleqtrd	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to j \in (0 ..^\|d\| + 1)$
104	103	ad2antrr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to j \in (0 ..^\|d\| + 1)$
105		simp-7r	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to d \in {Chain}_{A} \underset{˙}{\sim}$
106	105	chnwrd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to d \in Word A$
107		lencl	$⊢ d \in Word A \to \|d\| \in ℕ_{0}$
108		elnn0uz	$⊢ \|d\| \in ℕ_{0} \leftrightarrow \|d\| \in ℤ_{\geq 0}$
109	108	biimpi	$⊢ \|d\| \in ℕ_{0} \to \|d\| \in ℤ_{\geq 0}$
110	106 107 109	3syl	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to \|d\| \in ℤ_{\geq 0}$
111		fzosplitsni	$⊢ \|d\| \in ℤ_{\geq 0} \to (j \in (0 ..^\|d\| + 1) \leftrightarrow (j \in (0 ..^\|d\|) \lor j = \|d\|))$
112	110 111	syl	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to (j \in (0 ..^\|d\| + 1) \leftrightarrow (j \in (0 ..^\|d\|) \lor j = \|d\|))$
113	104 112	mpbid	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to (j \in (0 ..^\|d\|) \lor j = \|d\|)$
114		df-ne	$⊢ j \neq \|d\| \leftrightarrow \neg j = \|d\|$
115	114	bilani	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to \neg j = \|d\|$
116	113 115	olcnd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to j \in (0 ..^\|d\|)$
117	86 97 116	rspcdva	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \land j \neq \|d\|) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d)$
118	84 117	pm2.61dane	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d)$
119	71 118 81	ertrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} x$
120		simp-5r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to x \in A$
121	73 120 68	syl2anc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to lastS (d ++ ⟨“ x ”⟩) = x$
122	119 121	breqtrrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \land d \neq \emptyset) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩)$
123	70 122	pm2.61dane	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩)$
124	123	ralrimiva	$⊢ ((((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{\sim} x)) \land \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)) \to \forall j \in (0 ..^\|d ++ ⟨“ x ”⟩\|) (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d ++ ⟨“ x ”⟩)$
125	11 17 27 33 2 42 124	chnind	$⊢ φ \to \forall i \in (0 ..^\|C\|) C (i) \underset{˙}{\sim} lastS (C)$
126	5 125 3	rspcdva	$⊢ φ \to C (J) \underset{˙}{\sim} lastS (C)$

Metamath Proof Explorer

Theorem chnerlem1

Proof