chnub

Description: In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025)

	Ref	Expression
Hypotheses	chnub.1	$⊢ φ \to \underset{˙}{<} Po A$
	chnub.2	$⊢ φ \to C \in {Chain}_{A} \underset{˙}{<}$
	chnub.3	$⊢ φ \to I \in (0 ..^\|C\| - 1)$
Assertion	chnub	$⊢ φ \to C (I) \underset{˙}{<} lastS (C)$

Proof

Step	Hyp	Ref	Expression
1		chnub.1	$⊢ φ \to \underset{˙}{<} Po A$
2		chnub.2	$⊢ φ \to C \in {Chain}_{A} \underset{˙}{<}$
3		chnub.3	$⊢ φ \to I \in (0 ..^\|C\| - 1)$
4		fveq2	$⊢ i = I \to C (i) = C (I)$
5	4	breq1d	$⊢ i = I \to (C (i) \underset{˙}{<} lastS (C) \leftrightarrow C (I) \underset{˙}{<} lastS (C))$
6		fveq2	$⊢ c = \emptyset \to \|c\| = \|\emptyset\|$
7	6	oveq1d	$⊢ c = \emptyset \to \|c\| - 1 = \|\emptyset\| - 1$
8	7	oveq2d	$⊢ c = \emptyset \to (0 ..^\|c\| - 1) = (0 ..^\|\emptyset\| - 1)$
9		fveq1	$⊢ c = \emptyset \to c (i) = \emptyset (i)$
10		fveq2	$⊢ c = \emptyset \to lastS (c) = lastS (\emptyset)$
11	9 10	breq12d	$⊢ c = \emptyset \to (c (i) \underset{˙}{<} lastS (c) \leftrightarrow \emptyset (i) \underset{˙}{<} lastS (\emptyset))$
12	8 11	raleqbidv	$⊢ c = \emptyset \to (\forall i \in (0 ..^\|c\| - 1) c (i) \underset{˙}{<} lastS (c) \leftrightarrow \forall i \in (0 ..^\|\emptyset\| - 1) \emptyset (i) \underset{˙}{<} lastS (\emptyset))$
13		fveq2	$⊢ c = d \to \|c\| = \|d\|$
14	13	oveq1d	$⊢ c = d \to \|c\| - 1 = \|d\| - 1$
15	14	oveq2d	$⊢ c = d \to (0 ..^\|c\| - 1) = (0 ..^\|d\| - 1)$
16		fveq1	$⊢ c = d \to c (i) = d (i)$
17		fveq2	$⊢ c = d \to lastS (c) = lastS (d)$
18	16 17	breq12d	$⊢ c = d \to (c (i) \underset{˙}{<} lastS (c) \leftrightarrow d (i) \underset{˙}{<} lastS (d))$
19	15 18	raleqbidv	$⊢ c = d \to (\forall i \in (0 ..^\|c\| - 1) c (i) \underset{˙}{<} lastS (c) \leftrightarrow \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d))$
20		fveq2	$⊢ i = j \to c (i) = c (j)$
21	20	breq1d	$⊢ i = j \to (c (i) \underset{˙}{<} lastS (c) \leftrightarrow c (j) \underset{˙}{<} lastS (c))$
22	21	cbvralvw	$⊢ \forall i \in (0 ..^\|c\| - 1) c (i) \underset{˙}{<} lastS (c) \leftrightarrow \forall j \in (0 ..^\|c\| - 1) c (j) \underset{˙}{<} lastS (c)$
23		fveq2	$⊢ c = d ++ ⟨“ x ”⟩ \to \|c\| = \|d ++ ⟨“ x ”⟩\|$
24	23	oveq1d	$⊢ c = d ++ ⟨“ x ”⟩ \to \|c\| - 1 = \|d ++ ⟨“ x ”⟩\| - 1$
25	24	oveq2d	$⊢ c = d ++ ⟨“ x ”⟩ \to (0 ..^\|c\| - 1) = (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)$
26		fveq1	$⊢ c = d ++ ⟨“ x ”⟩ \to c (j) = (d ++ ⟨“ x ”⟩) (j)$
27		fveq2	$⊢ c = d ++ ⟨“ x ”⟩ \to lastS (c) = lastS (d ++ ⟨“ x ”⟩)$
28	26 27	breq12d	$⊢ c = d ++ ⟨“ x ”⟩ \to (c (j) \underset{˙}{<} lastS (c) \leftrightarrow (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩))$
29	25 28	raleqbidv	$⊢ c = d ++ ⟨“ x ”⟩ \to (\forall j \in (0 ..^\|c\| - 1) c (j) \underset{˙}{<} lastS (c) \leftrightarrow \forall j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩))$
30	22 29	bitrid	$⊢ c = d ++ ⟨“ x ”⟩ \to (\forall i \in (0 ..^\|c\| - 1) c (i) \underset{˙}{<} lastS (c) \leftrightarrow \forall j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩))$
31		fveq2	$⊢ c = C \to \|c\| = \|C\|$
32	31	oveq1d	$⊢ c = C \to \|c\| - 1 = \|C\| - 1$
33	32	oveq2d	$⊢ c = C \to (0 ..^\|c\| - 1) = (0 ..^\|C\| - 1)$
34		fveq1	$⊢ c = C \to c (i) = C (i)$
35		fveq2	$⊢ c = C \to lastS (c) = lastS (C)$
36	34 35	breq12d	$⊢ c = C \to (c (i) \underset{˙}{<} lastS (c) \leftrightarrow C (i) \underset{˙}{<} lastS (C))$
37	33 36	raleqbidv	$⊢ c = C \to (\forall i \in (0 ..^\|c\| - 1) c (i) \underset{˙}{<} lastS (c) \leftrightarrow \forall i \in (0 ..^\|C\| - 1) C (i) \underset{˙}{<} lastS (C))$
38		ral0	$⊢ \forall i \in \emptyset \emptyset (i) \underset{˙}{<} lastS (\emptyset)$
39		hash0	$⊢ \|\emptyset\| = 0$
40	39	oveq1i	$⊢ \|\emptyset\| - 1 = 0 - 1$
41		df-neg	$⊢ - 1 = 0 - 1$
42		neg1rr	$⊢ - 1 \in ℝ$
43		0re	$⊢ 0 \in ℝ$
44		neg1lt0	$⊢ - 1 < 0$
45	42 43 44	ltleii	$⊢ - 1 \leq 0$
46	41 45	eqbrtrri	$⊢ 0 - 1 \leq 0$
47	40 46	eqbrtri	$⊢ \|\emptyset\| - 1 \leq 0$
48		0z	$⊢ 0 \in ℤ$
49	39 48	eqeltri	$⊢ \|\emptyset\| \in ℤ$
50		1z	$⊢ 1 \in ℤ$
51		zsubcl	$⊢ (\|\emptyset\| \in ℤ \land 1 \in ℤ) \to \|\emptyset\| - 1 \in ℤ$
52	49 50 51	mp2an	$⊢ \|\emptyset\| - 1 \in ℤ$
53		fzon	$⊢ (0 \in ℤ \land \|\emptyset\| - 1 \in ℤ) \to (\|\emptyset\| - 1 \leq 0 \leftrightarrow (0 ..^\|\emptyset\| - 1) = \emptyset)$
54	48 52 53	mp2an	$⊢ \|\emptyset\| - 1 \leq 0 \leftrightarrow (0 ..^\|\emptyset\| - 1) = \emptyset$
55	47 54	mpbi	$⊢ (0 ..^\|\emptyset\| - 1) = \emptyset$
56	55	raleqi	$⊢ \forall i \in (0 ..^\|\emptyset\| - 1) \emptyset (i) \underset{˙}{<} lastS (\emptyset) \leftrightarrow \forall i \in \emptyset \emptyset (i) \underset{˙}{<} lastS (\emptyset)$
57	38 56	mpbir	$⊢ \forall i \in (0 ..^\|\emptyset\| - 1) \emptyset (i) \underset{˙}{<} lastS (\emptyset)$
58	57	a1i	$⊢ φ \to \forall i \in (0 ..^\|\emptyset\| - 1) \emptyset (i) \underset{˙}{<} lastS (\emptyset)$
59		simp-6r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to d \in {Chain}_{A} \underset{˙}{<}$
60	59	chnwrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to d \in Word A$
61		ccatws1len	$⊢ d \in Word A \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
62	60 61	syl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
63		simpr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to d = \emptyset$
64	63	fveq2d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d\| = \|\emptyset\|$
65	64 39	eqtrdi	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d\| = 0$
66	65	oveq1d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d\| + 1 = 0 + 1$
67		0p1e1	$⊢ 0 + 1 = 1$
68	67	a1i	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to 0 + 1 = 1$
69	62 66 68	3eqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d ++ ⟨“ x ”⟩\| = 1$
70	69	oveq1d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d ++ ⟨“ x ”⟩\| - 1 = 1 - 1$
71		1m1e0	$⊢ 1 - 1 = 0$
72	70 71	eqtrdi	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to \|d ++ ⟨“ x ”⟩\| - 1 = 0$
73	72	oveq2d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) = (0 ..^0)$
74		fzo0	$⊢ (0 ..^0) = \emptyset$
75	73 74	eqtrdi	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) = \emptyset$
76		simplr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)$
77	76	ne0d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) \neq \emptyset$
78	75 77	pm2.21ddne	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d = \emptyset) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
79	1	ad7antr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to \underset{˙}{<} Po A$
80		simp-6r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to d \in {Chain}_{A} \underset{˙}{<}$
81	80	chnwrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to d \in Word A$
82	81	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to d \in Word A$
83		simp-5r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to x \in A$
84	83	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to x \in A$
85		ccatws1cl	$⊢ (d \in Word A \land x \in A) \to d ++ ⟨“ x ”⟩ \in Word A$
86	82 84 85	syl2anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to d ++ ⟨“ x ”⟩ \in Word A$
87		lencl	$⊢ d \in Word A \to \|d\| \in ℕ_{0}$
88	81 87	syl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \in ℕ_{0}$
89	88	nn0zd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \in ℤ$
90		1zzd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to 1 \in ℤ$
91	89 90	zsubcld	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| - 1 \in ℤ$
92	89	peano2zd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| + 1 \in ℤ$
93	91	zred	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| - 1 \in ℝ$
94	92	zred	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| + 1 \in ℝ$
95		simpr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to d \neq \emptyset$
96		hasheq0	$⊢ d \in Word A \to (\|d\| = 0 \leftrightarrow d = \emptyset)$
97	96	necon3bid	$⊢ d \in Word A \to (\|d\| \neq 0 \leftrightarrow d \neq \emptyset)$
98	97	biimpar	$⊢ (d \in Word A \land d \neq \emptyset) \to \|d\| \neq 0$
99	81 95 98	syl2anc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \neq 0$
100		elnnne0	$⊢ \|d\| \in ℕ \leftrightarrow (\|d\| \in ℕ_{0} \land \|d\| \neq 0)$
101	88 99 100	sylanbrc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \in ℕ$
102	101	nnred	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \in ℝ$
103	102	ltm1d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| - 1 < \|d\|$
104	102	ltp1d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| < \|d\| + 1$
105	93 102 94 103 104	lttrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| - 1 < \|d\| + 1$
106	93 94 105	ltled	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| - 1 \leq \|d\| + 1$
107		eluz2	$⊢ \|d\| + 1 \in ℤ_{\geq (\|d\| - 1)} \leftrightarrow (\|d\| - 1 \in ℤ \land \|d\| + 1 \in ℤ \land \|d\| - 1 \leq \|d\| + 1)$
108	91 92 106 107	syl3anbrc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| + 1 \in ℤ_{\geq (\|d\| - 1)}$
109		fzoss2	$⊢ \|d\| + 1 \in ℤ_{\geq (\|d\| - 1)} \to (0 ..^\|d\| - 1) \subseteq (0 ..^\|d\| + 1)$
110	108 109	syl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to (0 ..^\|d\| - 1) \subseteq (0 ..^\|d\| + 1)$
111	110	sselda	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to j \in (0 ..^\|d\| + 1)$
112	82 61	syl	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
113	112	oveq2d	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to (0 ..^\|d ++ ⟨“ x ”⟩\|) = (0 ..^\|d\| + 1)$
114	111 113	eleqtrrd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)$
115		wrdsymbcl	$⊢ (d ++ ⟨“ x ”⟩ \in Word A \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\|)) \to (d ++ ⟨“ x ”⟩) (j) \in A$
116	86 114 115	syl2anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to (d ++ ⟨“ x ”⟩) (j) \in A$
117		simplr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to d \neq \emptyset$
118		lswcl	$⊢ (d \in Word A \land d \neq \emptyset) \to lastS (d) \in A$
119	82 117 118	syl2anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to lastS (d) \in A$
120		lswccats1	$⊢ (d \in Word A \land x \in A) \to lastS (d ++ ⟨“ x ”⟩) = x$
121	81 83 120	syl2anc	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to lastS (d ++ ⟨“ x ”⟩) = x$
122	121	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to lastS (d ++ ⟨“ x ”⟩) = x$
123	122 84	eqeltrd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to lastS (d ++ ⟨“ x ”⟩) \in A$
124	116 119 123	3jca	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to ((d ++ ⟨“ x ”⟩) (j) \in A \land lastS (d) \in A \land lastS (d ++ ⟨“ x ”⟩) \in A)$
125		simplr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)$
126	61	oveq1d	$⊢ d \in Word A \to \|d ++ ⟨“ x ”⟩\| - 1 = \|d\| + 1 - 1$
127	81 126	syl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d ++ ⟨“ x ”⟩\| - 1 = \|d\| + 1 - 1$
128	101	nncnd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \in ℂ$
129		1cnd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to 1 \in ℂ$
130	128 129	pncand	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| + 1 - 1 = \|d\|$
131	127 130	eqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d ++ ⟨“ x ”⟩\| - 1 = \|d\|$
132	131	oveq2d	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) = (0 ..^\|d\|)$
133	125 132	eleqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to j \in (0 ..^\|d\|)$
134	133	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to j \in (0 ..^\|d\|)$
135		ccats1val1	$⊢ (d \in Word A \land j \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (j) = d (j)$
136	82 134 135	syl2anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to (d ++ ⟨“ x ”⟩) (j) = d (j)$
137		fveq2	$⊢ i = j \to d (i) = d (j)$
138	137	breq1d	$⊢ i = j \to (d (i) \underset{˙}{<} lastS (d) \leftrightarrow d (j) \underset{˙}{<} lastS (d))$
139		simp-4r	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)$
140		simpr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to j \in (0 ..^\|d\| - 1)$
141	138 139 140	rspcdva	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to d (j) \underset{˙}{<} lastS (d)$
142	136 141	eqbrtrd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d)$
143		simp-4r	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to (d = \emptyset \lor lastS (d) \underset{˙}{<} x)$
144	95	neneqd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \neg d = \emptyset$
145	143 144	orcnd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to lastS (d) \underset{˙}{<} x$
146	145	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to lastS (d) \underset{˙}{<} x$
147	146 122	breqtrrd	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to lastS (d) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
148		potr	$⊢ (\underset{˙}{<} Po A \land ((d ++ ⟨“ x ”⟩) (j) \in A \land lastS (d) \in A \land lastS (d ++ ⟨“ x ”⟩) \in A)) \to (((d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d) \land lastS (d) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩))$
149	148	imp	$⊢ ((\underset{˙}{<} Po A \land ((d ++ ⟨“ x ”⟩) (j) \in A \land lastS (d) \in A \land lastS (d ++ ⟨“ x ”⟩) \in A)) \land ((d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d) \land lastS (d) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩))) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
150	79 124 142 147 149	syl22anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j \in (0 ..^\|d\| - 1)) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
151	145	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to lastS (d) \underset{˙}{<} x$
152	81	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to d \in Word A$
153		simp-6r	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to x \in A$
154	153	s1cld	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to ⟨“ x ”⟩ \in Word A$
155	101	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to \|d\| \in ℕ$
156		fzo0end	$⊢ \|d\| \in ℕ \to \|d\| - 1 \in (0 ..^\|d\|)$
157	155 156	syl	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to \|d\| - 1 \in (0 ..^\|d\|)$
158		ccatval1	$⊢ (d \in Word A \land ⟨“ x ”⟩ \in Word A \land \|d\| - 1 \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (\|d\| - 1) = d (\|d\| - 1)$
159	152 154 157 158	syl3anc	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to (d ++ ⟨“ x ”⟩) (\|d\| - 1) = d (\|d\| - 1)$
160		simpr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to j = \|d\| - 1$
161	160	fveq2d	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to (d ++ ⟨“ x ”⟩) (j) = (d ++ ⟨“ x ”⟩) (\|d\| - 1)$
162		lsw	$⊢ d \in Word A \to lastS (d) = d (\|d\| - 1)$
163	152 162	syl	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to lastS (d) = d (\|d\| - 1)$
164	159 161 163	3eqtr4d	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to (d ++ ⟨“ x ”⟩) (j) = lastS (d)$
165	121	adantr	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to lastS (d ++ ⟨“ x ”⟩) = x$
166	151 164 165	3brtr4d	$⊢ (((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \land j = \|d\| - 1) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
167	67	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
168		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
169	167 168	eqtr4i	$⊢ ℤ_{\geq (0 + 1)} = ℕ$
170	101 169	eleqtrrdi	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to \|d\| \in ℤ_{\geq (0 + 1)}$
171		fzosplitsnm1	$⊢ (0 \in ℤ \land \|d\| \in ℤ_{\geq (0 + 1)}) \to (0 ..^\|d\|) = (0 ..^\|d\| - 1) \cup \{\|d\| - 1\}$
172	48 170 171	sylancr	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to (0 ..^\|d\|) = (0 ..^\|d\| - 1) \cup \{\|d\| - 1\}$
173	133 172	eleqtrd	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to j \in ((0 ..^\|d\| - 1) \cup \{\|d\| - 1\})$
174		elunsn	$⊢ j \in ((0 ..^\|d\| - 1) \cup \{\|d\| - 1\}) \to (j \in ((0 ..^\|d\| - 1) \cup \{\|d\| - 1\}) \leftrightarrow (j \in (0 ..^\|d\| - 1) \lor j = \|d\| - 1))$
175	174	ibi	$⊢ j \in ((0 ..^\|d\| - 1) \cup \{\|d\| - 1\}) \to (j \in (0 ..^\|d\| - 1) \lor j = \|d\| - 1)$
176	173 175	syl	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to (j \in (0 ..^\|d\| - 1) \lor j = \|d\| - 1)$
177	150 166 176	mpjaodan	$⊢ ((((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \land d \neq \emptyset) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
178	78 177	pm2.61dane	$⊢ (((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \land j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1)) \to (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
179	178	ralrimiva	$⊢ ((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land \forall i \in (0 ..^\|d\| - 1) d (i) \underset{˙}{<} lastS (d)) \to \forall j \in (0 ..^\|d ++ ⟨“ x ”⟩\| - 1) (d ++ ⟨“ x ”⟩) (j) \underset{˙}{<} lastS (d ++ ⟨“ x ”⟩)$
180	12 19 30 37 2 58 179	chnind	$⊢ φ \to \forall i \in (0 ..^\|C\| - 1) C (i) \underset{˙}{<} lastS (C)$
181	5 180 3	rspcdva	$⊢ φ \to C (I) \underset{˙}{<} lastS (C)$

Metamath Proof Explorer

Theorem chnub

Proof