chnind

Description: Induction over a chain. See nnind for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025)

	Ref	Expression
Hypotheses	chnind.1	$⊢ c = \emptyset \to (ψ \leftrightarrow χ)$
	chnind.2	$⊢ c = d \to (ψ \leftrightarrow θ)$
	chnind.3	$⊢ c = d ++ ⟨“ x ”⟩ \to (ψ \leftrightarrow τ)$
	chnind.4	$⊢ c = C \to (ψ \leftrightarrow η)$
	chnind.6	$⊢ φ \to C \in {Chain}_{A} \underset{˙}{<}$
	chnind.7	$⊢ φ \to χ$
	chnind.8	$⊢ ((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land θ) \to τ$
Assertion	chnind	$⊢ φ \to η$

Proof

Step	Hyp	Ref	Expression
1		chnind.1	$⊢ c = \emptyset \to (ψ \leftrightarrow χ)$
2		chnind.2	$⊢ c = d \to (ψ \leftrightarrow θ)$
3		chnind.3	$⊢ c = d ++ ⟨“ x ”⟩ \to (ψ \leftrightarrow τ)$
4		chnind.4	$⊢ c = C \to (ψ \leftrightarrow η)$
5		chnind.6	$⊢ φ \to C \in {Chain}_{A} \underset{˙}{<}$
6		chnind.7	$⊢ φ \to χ$
7		chnind.8	$⊢ ((((φ \land d \in {Chain}_{A} \underset{˙}{<}) \land x \in A) \land (d = \emptyset \lor lastS (d) \underset{˙}{<} x)) \land θ) \to τ$
8	5	chnwrd	$⊢ φ \to C \in Word A$
9		id	$⊢ φ \to φ$
10		ischn	$⊢ C \in {Chain}_{A} \underset{˙}{<} \leftrightarrow (C \in Word A \land \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i))$
11	5 10	sylib	$⊢ φ \to (C \in Word A \land \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i))$
12	11	simprd	$⊢ φ \to \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i)$
13		dmeq	$⊢ c = \emptyset \to dom c = dom \emptyset$
14	13	difeq1d	$⊢ c = \emptyset \to dom c ∖ \{0\} = dom \emptyset ∖ \{0\}$
15		fveq1	$⊢ c = \emptyset \to c (i - 1) = \emptyset (i - 1)$
16		fveq1	$⊢ c = \emptyset \to c (i) = \emptyset (i)$
17	15 16	breq12d	$⊢ c = \emptyset \to (c (i - 1) \underset{˙}{<} c (i) \leftrightarrow \emptyset (i - 1) \underset{˙}{<} \emptyset (i))$
18	14 17	raleqbidv	$⊢ c = \emptyset \to (\forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i) \leftrightarrow \forall i \in (dom \emptyset ∖ \{0\}) \emptyset (i - 1) \underset{˙}{<} \emptyset (i))$
19	18	anbi2d	$⊢ c = \emptyset \to ((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \leftrightarrow (φ \land \forall i \in (dom \emptyset ∖ \{0\}) \emptyset (i - 1) \underset{˙}{<} \emptyset (i)))$
20	19 1	imbi12d	$⊢ c = \emptyset \to (((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \to ψ) \leftrightarrow ((φ \land \forall i \in (dom \emptyset ∖ \{0\}) \emptyset (i - 1) \underset{˙}{<} \emptyset (i)) \to χ))$
21		dmeq	$⊢ c = d \to dom c = dom d$
22	21	difeq1d	$⊢ c = d \to dom c ∖ \{0\} = dom d ∖ \{0\}$
23		fveq1	$⊢ c = d \to c (i - 1) = d (i - 1)$
24		fveq1	$⊢ c = d \to c (i) = d (i)$
25	23 24	breq12d	$⊢ c = d \to (c (i - 1) \underset{˙}{<} c (i) \leftrightarrow d (i - 1) \underset{˙}{<} d (i))$
26	22 25	raleqbidv	$⊢ c = d \to (\forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i) \leftrightarrow \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i))$
27	26	anbi2d	$⊢ c = d \to ((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \leftrightarrow (φ \land \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i)))$
28	27 2	imbi12d	$⊢ c = d \to (((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \to ψ) \leftrightarrow ((φ \land \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i)) \to θ))$
29		dmeq	$⊢ c = d ++ ⟨“ x ”⟩ \to dom c = dom (d ++ ⟨“ x ”⟩)$
30	29	difeq1d	$⊢ c = d ++ ⟨“ x ”⟩ \to dom c ∖ \{0\} = dom (d ++ ⟨“ x ”⟩) ∖ \{0\}$
31		fveq1	$⊢ c = d ++ ⟨“ x ”⟩ \to c (i - 1) = (d ++ ⟨“ x ”⟩) (i - 1)$
32		fveq1	$⊢ c = d ++ ⟨“ x ”⟩ \to c (i) = (d ++ ⟨“ x ”⟩) (i)$
33	31 32	breq12d	$⊢ c = d ++ ⟨“ x ”⟩ \to (c (i - 1) \underset{˙}{<} c (i) \leftrightarrow (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i))$
34	30 33	raleqbidv	$⊢ c = d ++ ⟨“ x ”⟩ \to (\forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i) \leftrightarrow \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i))$
35	34	anbi2d	$⊢ c = d ++ ⟨“ x ”⟩ \to ((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \leftrightarrow (φ \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)))$
36	35 3	imbi12d	$⊢ c = d ++ ⟨“ x ”⟩ \to (((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \to ψ) \leftrightarrow ((φ \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to τ))$
37		dmeq	$⊢ c = C \to dom c = dom C$
38	37	difeq1d	$⊢ c = C \to dom c ∖ \{0\} = dom C ∖ \{0\}$
39		fveq1	$⊢ c = C \to c (i - 1) = C (i - 1)$
40		fveq1	$⊢ c = C \to c (i) = C (i)$
41	39 40	breq12d	$⊢ c = C \to (c (i - 1) \underset{˙}{<} c (i) \leftrightarrow C (i - 1) \underset{˙}{<} C (i))$
42	38 41	raleqbidv	$⊢ c = C \to (\forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i) \leftrightarrow \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i))$
43	42	anbi2d	$⊢ c = C \to ((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \leftrightarrow (φ \land \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i)))$
44	43 4	imbi12d	$⊢ c = C \to (((φ \land \forall i \in (dom c ∖ \{0\}) c (i - 1) \underset{˙}{<} c (i)) \to ψ) \leftrightarrow ((φ \land \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i)) \to η))$
45	6	adantr	$⊢ (φ \land \forall i \in (dom \emptyset ∖ \{0\}) \emptyset (i - 1) \underset{˙}{<} \emptyset (i)) \to χ$
46		simpllr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to φ$
47		simp-4l	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to d \in Word A$
48		simpll	$⊢ ((d \in Word A \land x \in A) \land φ) \to d \in Word A$
49		simplr	$⊢ ((d \in Word A \land x \in A) \land φ) \to x \in A$
50	49	s1cld	$⊢ ((d \in Word A \land x \in A) \land φ) \to ⟨“ x ”⟩ \in Word A$
51	48 50	ccatdmss	$⊢ ((d \in Word A \land x \in A) \land φ) \to dom d \subseteq dom (d ++ ⟨“ x ”⟩)$
52	51	ssdifd	$⊢ ((d \in Word A \land x \in A) \land φ) \to dom d ∖ \{0\} \subseteq dom (d ++ ⟨“ x ”⟩) ∖ \{0\}$
53	52	sselda	$⊢ (((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \to j \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\})$
54		fvoveq1	$⊢ i = j \to (d ++ ⟨“ x ”⟩) (i - 1) = (d ++ ⟨“ x ”⟩) (j - 1)$
55		fveq2	$⊢ i = j \to (d ++ ⟨“ x ”⟩) (i) = (d ++ ⟨“ x ”⟩) (j)$
56	54 55	breq12d	$⊢ i = j \to ((d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i) \leftrightarrow (d ++ ⟨“ x ”⟩) (j - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (j))$
57	56	adantl	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land i = j) \to ((d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i) \leftrightarrow (d ++ ⟨“ x ”⟩) (j - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (j))$
58	53 57	rspcdv	$⊢ (((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \to (\forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i) \to (d ++ ⟨“ x ”⟩) (j - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (j))$
59	58	imp	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (d ++ ⟨“ x ”⟩) (j - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (j)$
60		simp-4l	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to d \in Word A$
61	50	ad2antrr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to ⟨“ x ”⟩ \in Word A$
62		lencl	$⊢ d \in Word A \to \|d\| \in ℕ_{0}$
63	60 62	syl	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| \in ℕ_{0}$
64	63	nn0zd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| \in ℤ$
65		fzossrbm1	$⊢ \|d\| \in ℤ \to (0 ..^\|d\| - 1) \subseteq (0 ..^\|d\|)$
66	64 65	syl	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (0 ..^\|d\| - 1) \subseteq (0 ..^\|d\|)$
67		fzossz	$⊢ (0 ..^\|d\|) \subseteq ℤ$
68		simplr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j \in (dom d ∖ \{0\})$
69	68	eldifad	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j \in dom d$
70		eqidd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| = \|d\|$
71	70 60	wrdfd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to d : (0 ..^\|d\|) ⟶ A$
72	71	fdmd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to dom d = (0 ..^\|d\|)$
73	69 72	eleqtrd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j \in (0 ..^\|d\|)$
74	67 73	sselid	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j \in ℤ$
75		eldifsni	$⊢ j \in (dom d ∖ \{0\}) \to j \neq 0$
76	68 75	syl	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j \neq 0$
77		fzo1fzo0n0	$⊢ j \in (1 ..^\|d\|) \leftrightarrow (j \in (0 ..^\|d\|) \land j \neq 0)$
78	73 76 77	sylanbrc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j \in (1 ..^\|d\|)$
79		elfzom1b	$⊢ (j \in ℤ \land \|d\| \in ℤ) \to (j \in (1 ..^\|d\|) \leftrightarrow j - 1 \in (0 ..^\|d\| - 1))$
80	79	biimpa	$⊢ ((j \in ℤ \land \|d\| \in ℤ) \land j \in (1 ..^\|d\|)) \to j - 1 \in (0 ..^\|d\| - 1)$
81	74 64 78 80	syl21anc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j - 1 \in (0 ..^\|d\| - 1)$
82	66 81	sseldd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to j - 1 \in (0 ..^\|d\|)$
83		ccatval1	$⊢ (d \in Word A \land ⟨“ x ”⟩ \in Word A \land j - 1 \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (j - 1) = d (j - 1)$
84	60 61 82 83	syl3anc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (d ++ ⟨“ x ”⟩) (j - 1) = d (j - 1)$
85		ccatval1	$⊢ (d \in Word A \land ⟨“ x ”⟩ \in Word A \land j \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (j) = d (j)$
86	60 61 73 85	syl3anc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (d ++ ⟨“ x ”⟩) (j) = d (j)$
87	59 84 86	3brtr3d	$⊢ ((((d \in Word A \land x \in A) \land φ) \land j \in (dom d ∖ \{0\})) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to d (j - 1) \underset{˙}{<} d (j)$
88	87	an32s	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land j \in (dom d ∖ \{0\})) \to d (j - 1) \underset{˙}{<} d (j)$
89	88	adantllr	$⊢ (((((d \in Word A \land x \in A) \land φ) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land j \in (dom d ∖ \{0\})) \to d (j - 1) \underset{˙}{<} d (j)$
90	89	ralrimiva	$⊢ ((((d \in Word A \land x \in A) \land φ) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \forall j \in (dom d ∖ \{0\}) d (j - 1) \underset{˙}{<} d (j)$
91	90	an32s	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to \forall j \in (dom d ∖ \{0\}) d (j - 1) \underset{˙}{<} d (j)$
92		ischn	$⊢ d \in {Chain}_{A} \underset{˙}{<} \leftrightarrow (d \in Word A \land \forall j \in (dom d ∖ \{0\}) d (j - 1) \underset{˙}{<} d (j))$
93	47 91 92	sylanbrc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to d \in {Chain}_{A} \underset{˙}{<}$
94	46 93	jca	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to (φ \land d \in {Chain}_{A} \underset{˙}{<})$
95		simp-4r	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to x \in A$
96		lsw	$⊢ d \in Word A \to lastS (d) = d (\|d\| - 1)$
97	96	ad5antr	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to lastS (d) = d (\|d\| - 1)$
98		simp-4l	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to d \in Word A$
99		fzonn0p1	$⊢ \|d\| \in ℕ_{0} \to \|d\| \in (0 ..^\|d\| + 1)$
100	98 62 99	3syl	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \|d\| \in (0 ..^\|d\| + 1)$
101		ccatws1len	$⊢ d \in Word A \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
102	101	ad4antr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \|d ++ ⟨“ x ”⟩\| = \|d\| + 1$
103	102	eqcomd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \|d\| + 1 = \|d ++ ⟨“ x ”⟩\|$
104		ccatws1cl	$⊢ (d \in Word A \land x \in A) \to d ++ ⟨“ x ”⟩ \in Word A$
105	104	ad3antrrr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to d ++ ⟨“ x ”⟩ \in Word A$
106	103 105	wrdfd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to (d ++ ⟨“ x ”⟩) : (0 ..^\|d\| + 1) ⟶ A$
107	106	fdmd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to dom (d ++ ⟨“ x ”⟩) = (0 ..^\|d\| + 1)$
108	100 107	eleqtrrd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \|d\| \in dom (d ++ ⟨“ x ”⟩)$
109		simplr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \neg d = \emptyset$
110	109	neqned	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to d \neq \emptyset$
111		hasheq0	$⊢ d \in Word A \to (\|d\| = 0 \leftrightarrow d = \emptyset)$
112	111	necon3bid	$⊢ d \in Word A \to (\|d\| \neq 0 \leftrightarrow d \neq \emptyset)$
113	112	biimpar	$⊢ (d \in Word A \land d \neq \emptyset) \to \|d\| \neq 0$
114	98 110 113	syl2anc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \|d\| \neq 0$
115	108 114	eldifsnd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to \|d\| \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\})$
116		fvoveq1	$⊢ i = \|d\| \to (d ++ ⟨“ x ”⟩) (i - 1) = (d ++ ⟨“ x ”⟩) (\|d\| - 1)$
117		fveq2	$⊢ i = \|d\| \to (d ++ ⟨“ x ”⟩) (i) = (d ++ ⟨“ x ”⟩) (\|d\|)$
118	116 117	breq12d	$⊢ i = \|d\| \to ((d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i) \leftrightarrow (d ++ ⟨“ x ”⟩) (\|d\| - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (\|d\|))$
119	118	adantl	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land i = \|d\|) \to ((d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i) \leftrightarrow (d ++ ⟨“ x ”⟩) (\|d\| - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (\|d\|))$
120	115 119	rspcdv	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \to (\forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i) \to (d ++ ⟨“ x ”⟩) (\|d\| - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (\|d\|))$
121	120	imp	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (d ++ ⟨“ x ”⟩) (\|d\| - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (\|d\|)$
122	48	ad3antrrr	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to d \in Word A$
123	50	ad3antrrr	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to ⟨“ x ”⟩ \in Word A$
124	122 62	syl	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| \in ℕ_{0}$
125	114	adantr	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| \neq 0$
126		elnnne0	$⊢ \|d\| \in ℕ \leftrightarrow (\|d\| \in ℕ_{0} \land \|d\| \neq 0)$
127	124 125 126	sylanbrc	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| \in ℕ$
128		fzo0end	$⊢ \|d\| \in ℕ \to \|d\| - 1 \in (0 ..^\|d\|)$
129	127 128	syl	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| - 1 \in (0 ..^\|d\|)$
130		ccatval1	$⊢ (d \in Word A \land ⟨“ x ”⟩ \in Word A \land \|d\| - 1 \in (0 ..^\|d\|)) \to (d ++ ⟨“ x ”⟩) (\|d\| - 1) = d (\|d\| - 1)$
131	122 123 129 130	syl3anc	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (d ++ ⟨“ x ”⟩) (\|d\| - 1) = d (\|d\| - 1)$
132	49	ad3antrrr	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to x \in A$
133		eqidd	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \|d\| = \|d\|$
134		ccats1val2	$⊢ (d \in Word A \land x \in A \land \|d\| = \|d\|) \to (d ++ ⟨“ x ”⟩) (\|d\|) = x$
135	122 132 133 134	syl3anc	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (d ++ ⟨“ x ”⟩) (\|d\|) = x$
136	121 131 135	3brtr3d	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to d (\|d\| - 1) \underset{˙}{<} x$
137	97 136	eqbrtrd	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \neg d = \emptyset) \land θ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to lastS (d) \underset{˙}{<} x$
138	137	an42ds	$⊢ (((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \land \neg d = \emptyset) \to lastS (d) \underset{˙}{<} x$
139	138	ex	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to (\neg d = \emptyset \to lastS (d) \underset{˙}{<} x)$
140	139	orrd	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to (d = \emptyset \lor lastS (d) \underset{˙}{<} x)$
141		simpr	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to θ$
142	94 95 140 141 7	syl1111anc	$⊢ ((((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \land θ) \to τ$
143	142	ex	$⊢ (((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (θ \to τ)$
144	143	expl	$⊢ (d \in Word A \land x \in A) \to ((φ \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to (θ \to τ))$
145	88	ralrimiva	$⊢ (((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \forall j \in (dom d ∖ \{0\}) d (j - 1) \underset{˙}{<} d (j)$
146		fvoveq1	$⊢ i = j \to d (i - 1) = d (j - 1)$
147		fveq2	$⊢ i = j \to d (i) = d (j)$
148	146 147	breq12d	$⊢ i = j \to (d (i - 1) \underset{˙}{<} d (i) \leftrightarrow d (j - 1) \underset{˙}{<} d (j))$
149	148	cbvralvw	$⊢ \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i) \leftrightarrow \forall j \in (dom d ∖ \{0\}) d (j - 1) \underset{˙}{<} d (j)$
150	145 149	sylibr	$⊢ (((d \in Word A \land x \in A) \land φ) \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i)$
151	150	expl	$⊢ (d \in Word A \land x \in A) \to ((φ \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i))$
152	144 151	a2and	$⊢ (d \in Word A \land x \in A) \to (((φ \land \forall i \in (dom d ∖ \{0\}) d (i - 1) \underset{˙}{<} d (i)) \to θ) \to ((φ \land \forall i \in (dom (d ++ ⟨“ x ”⟩) ∖ \{0\}) (d ++ ⟨“ x ”⟩) (i - 1) \underset{˙}{<} (d ++ ⟨“ x ”⟩) (i)) \to τ))$
153	20 28 36 44 45 152	wrdind	$⊢ C \in Word A \to ((φ \land \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i)) \to η)$
154	153	imp	$⊢ (C \in Word A \land (φ \land \forall i \in (dom C ∖ \{0\}) C (i - 1) \underset{˙}{<} C (i))) \to η$
155	8 9 12 154	syl12anc	$⊢ φ \to η$

Metamath Proof Explorer

Theorem chnind

Proof