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		0nnn	$⊢ \neg 0 \in ℕ$
35		hash0	$⊢ \|\emptyset\| = 0$
36	35	eleq1i	$⊢ \|\emptyset\| \in ℕ \leftrightarrow 0 \in ℕ$
37	34 36	mtbir	$⊢ \neg \|\emptyset\| \in ℕ$
38		fzo0n0	$⊢ (0 ..^\|\emptyset\|) \neq \emptyset \leftrightarrow \|\emptyset\| \in ℕ$
39	37 38	mtbir	$⊢ \neg (0 ..^\|\emptyset\|) \neq \emptyset$
40		nne	$⊢ \neg (0 ..^\|\emptyset\|) \neq \emptyset \leftrightarrow (0 ..^\|\emptyset\|) = \emptyset$
41	39 40	mpbi	$⊢ (0 ..^\|\emptyset\|) = \emptyset$
42		rzal	$⊢ (0 ..^\|\emptyset\|) = \emptyset \to \forall i \in (0 ..^\|\emptyset\|) \emptyset (i) \underset{˙}{\sim} lastS (\emptyset)$
43	41 42	mp1i	$⊢ φ \to \forall i \in (0 ..^\|\emptyset\|) \emptyset (i) \underset{˙}{\sim} lastS (\emptyset)$
44	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$
45		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$
46	44 45	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$
47		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}$
48	47	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$
49		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 ”⟩\|)$
50		ccatws1len	$⊢ d \in Word A \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
51	48 50	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$
52		fveq2	$⊢ d = \emptyset \to \|d\| = \|\emptyset\|$
53	52 35	eqtr2di	$⊢ d = \emptyset \to 0 = \|d\|$
54	53	eqcomd	$⊢ d = \emptyset \to \|d\| = 0$
55	54	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$
56	55	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$
57		0p1e1	$⊢ 0 + 1 = 1$
58	56 57	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$
59	51 58	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$
60	59	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)$
61	49 60	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)$
62		fzo01	$⊢ (0 ..^1) = \{0\}$
63	62	a1i	$⊢ ((((((φ \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 ..^1) = \{0\}$
64	61 63	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\}$
65		elsni	$⊢ j \in \{0\} \to j = 0$
66	64 65	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 j = 0$
67	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 0 = \|d\|$
68	66 67	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\|$
69		ccats1val2	$⊢ (d \in Word A \land x \in A \land j = \|d\|) \to (d ++ ⟨“ x ”⟩) (j) = x$
70	48 45 68 69	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$
71		lswccats1	$⊢ (d \in Word A \land x \in A) \to lastS (d ++ ⟨“ x ”⟩) = x$
72	48 45 71	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$
73	46 70 72	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 ”⟩)$
74	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$
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) \to d \in {Chain}_{A} \underset{˙}{\sim}$
76	75	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$
77	76	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$
78		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$
79		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\|$
80	77 78 79 69	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$
81		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)$
82		neneq	$⊢ d \neq \emptyset \to \neg d = \emptyset$
83	82	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$
84	81 83	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$
85	74 84	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)$
86	85	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)$
87	80 86	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)$
88		fveq2	$⊢ i = j \to (d ++ ⟨“ x ”⟩) (i) = (d ++ ⟨“ x ”⟩) (j)$
89	88	breq1d	$⊢ i = j \to ((d ++ ⟨“ x ”⟩) (i) \underset{˙}{\sim} lastS (d) \leftrightarrow (d ++ ⟨“ x ”⟩) (j) \underset{˙}{\sim} lastS (d))$
90		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)) \to \forall i \in (0 ..^\|d\|) d (i) \underset{˙}{\sim} lastS (d)$
91	90	ad3antrrr	$⊢ (((((((φ \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)$
92		simplr	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to d \in {Chain}_{A} \underset{˙}{\sim}$
93	92	chnwrd	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to d \in Word A$
94		simpr	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to i \in (0 ..^\|d\|)$
95		ccats1val1	$⊢ (d \in Word A \land i \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (i) = d (i)$
96	93 94 95	syl2anc	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (i) = d (i)$
97	96	eqcomd	$⊢ ((φ \land d \in {Chain}_{A} \underset{˙}{\sim}) \land i \in (0 ..^\|d\|)) \to d (i) = (d ++ ⟨“ x ”⟩) (i)$
98	97	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))$
99	98	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))$
100	99	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))$
101	91 100	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)$
102		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 ”⟩\|)$
103		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}$
104	103	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$
105	104 50	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$
106	105	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)$
107	102 106	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)$
108	107	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)$
109		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}$
110	109	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$
111		lencl	$⊢ d \in Word A \to \|d\| \in ℕ_{0}$
112		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
113	112	eleq2i	$⊢ \|d\| \in ℕ_{0} \leftrightarrow \|d\| \in ℤ_{\geq 0}$
114	113	biimpi	$⊢ \|d\| \in ℕ_{0} \to \|d\| \in ℤ_{\geq 0}$
115	110 111 114	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}$
116		fzosplitsni	$⊢ \|d\| \in ℤ_{\geq 0} \to (j \in (0 ..^\|d\| + 1) \leftrightarrow (j \in (0 ..^\|d\|) \lor j = \|d\|))$
117	115 116	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\|))$
118	108 117	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\|)$
119		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 \neq \|d\|) \to j \neq \|d\|$
120		df-ne	$⊢ j \neq \|d\| \leftrightarrow \neg j = \|d\|$
121	119 120	sylib	$⊢ (((((((φ \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\|$
122	118 121	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\|)$
123	89 101 122	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)$
124	87 123	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)$
125	74 124 84	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$
126		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$
127	76 126 71	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$
128	125 127	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 ”⟩)$
129	73 128	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 ”⟩)$
130	129	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 ”⟩)$
131	11 17 27 33 2 43 130	chnind	$⊢ φ \to \forall i \in (0 ..^\|C\|) C (i) \underset{˙}{\sim} lastS (C)$
132	5 131 3	rspcdva	$⊢ φ \to C (J) \underset{˙}{\sim} lastS (C)$

Metamath Proof Explorer

Theorem chnerlem1

Proof