chnerlem1 - Mathbox for Ender Ting

	Mathbox for Ender Ting		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > chnerlem1		Structured version Visualization version GIF version

Theorem chnerlem1 47718

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

**Hypotheses**
Ref	Expression
chner.1	⊢ (𝜑 → ∼ Er 𝐴)
chner.2	⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))
chner.3	⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))

**Assertion**
Ref	Expression
chnerlem1	⊢ (𝜑 → (𝐶‘𝐽) ∼ (lastS‘𝐶))

Proof of Theorem chnerlem1 Dummy variables 𝑐 𝑑 𝑖 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6882	. . 3 ⊢ (𝑖 = 𝐽 → (𝐶‘𝑖) = (𝐶‘𝐽))
2	1	breq1d 5117	. 2 ⊢ (𝑖 = 𝐽 → ((𝐶‘𝑖) ∼ (lastS‘𝐶) ↔ (𝐶‘𝐽) ∼ (lastS‘𝐶)))
3		fveq2 6882	. . . . 5 ⊢ (𝑐 = ∅ → (♯‘𝑐) = (♯‘∅))
4	3	oveq2d 7433	. . . 4 ⊢ (𝑐 = ∅ → (0..^(♯‘𝑐)) = (0..^(♯‘∅)))
5		fveq1 6881	. . . . 5 ⊢ (𝑐 = ∅ → (𝑐‘𝑖) = (∅‘𝑖))
6		fveq2 6882	. . . . 5 ⊢ (𝑐 = ∅ → (lastS‘𝑐) = (lastS‘∅))
7	5, 6	breq12d 5120	. . . 4 ⊢ (𝑐 = ∅ → ((𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ (∅‘𝑖) ∼ (lastS‘∅)))
8	4, 7	raleqbidv 3336	. . 3 ⊢ (𝑐 = ∅ → (∀𝑖 ∈ (0..^(♯‘𝑐))(𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ ∀𝑖 ∈ (0..^(♯‘∅))(∅‘𝑖) ∼ (lastS‘∅)))
9		fveq2 6882	. . . . 5 ⊢ (𝑐 = 𝑑 → (♯‘𝑐) = (♯‘𝑑))
10	9	oveq2d 7433	. . . 4 ⊢ (𝑐 = 𝑑 → (0..^(♯‘𝑐)) = (0..^(♯‘𝑑)))
11		fveq1 6881	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑐‘𝑖) = (𝑑‘𝑖))
12		fveq2 6882	. . . . 5 ⊢ (𝑐 = 𝑑 → (lastS‘𝑐) = (lastS‘𝑑))
13	11, 12	breq12d 5120	. . . 4 ⊢ (𝑐 = 𝑑 → ((𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ (𝑑‘𝑖) ∼ (lastS‘𝑑)))
14	10, 13	raleqbidv 3336	. . 3 ⊢ (𝑐 = 𝑑 → (∀𝑖 ∈ (0..^(♯‘𝑐))(𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)))
15		fveq2 6882	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗))
16	15	breq1d 5117	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ (𝑐‘𝑗) ∼ (lastS‘𝑐)))
17	16	cbvralvw 3242	. . . 4 ⊢ (∀𝑖 ∈ (0..^(♯‘𝑐))(𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ ∀𝑗 ∈ (0..^(♯‘𝑐))(𝑐‘𝑗) ∼ (lastS‘𝑐))
18		fveq2 6882	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (♯‘𝑐) = (♯‘(𝑑 ++ ⟨“𝑥”⟩)))
19	18	oveq2d 7433	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (0..^(♯‘𝑐)) = (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))))
20		fveq1 6881	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝑐‘𝑗) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
21		fveq2 6882	. . . . . 6 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (lastS‘𝑐) = (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
22	20, 21	breq12d 5120	. . . . 5 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → ((𝑐‘𝑗) ∼ (lastS‘𝑐) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
23	19, 22	raleqbidv 3336	. . . 4 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑗 ∈ (0..^(♯‘𝑐))(𝑐‘𝑗) ∼ (lastS‘𝑐) ↔ ∀𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
24	17, 23	bitrid 286	. . 3 ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (∀𝑖 ∈ (0..^(♯‘𝑐))(𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ ∀𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩))))
25		fveq2 6882	. . . . 5 ⊢ (𝑐 = 𝐶 → (♯‘𝑐) = (♯‘𝐶))
26	25	oveq2d 7433	. . . 4 ⊢ (𝑐 = 𝐶 → (0..^(♯‘𝑐)) = (0..^(♯‘𝐶)))
27		fveq1 6881	. . . . 5 ⊢ (𝑐 = 𝐶 → (𝑐‘𝑖) = (𝐶‘𝑖))
28		fveq2 6882	. . . . 5 ⊢ (𝑐 = 𝐶 → (lastS‘𝑐) = (lastS‘𝐶))
29	27, 28	breq12d 5120	. . . 4 ⊢ (𝑐 = 𝐶 → ((𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ (𝐶‘𝑖) ∼ (lastS‘𝐶)))
30	26, 29	raleqbidv 3336	. . 3 ⊢ (𝑐 = 𝐶 → (∀𝑖 ∈ (0..^(♯‘𝑐))(𝑐‘𝑖) ∼ (lastS‘𝑐) ↔ ∀𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) ∼ (lastS‘𝐶)))
31		chner.2	. . 3 ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))
32		hash0 14435	. . . . . . 7 ⊢ (♯‘∅) = 0
33		0nnn 12300	. . . . . . 7 ⊢ ¬ 0 ∈ ℕ
34	32, 33	eqneltri 2881	. . . . . 6 ⊢ ¬ (♯‘∅) ∈ ℕ
35		fzo0n0 13776	. . . . . 6 ⊢ ((0..^(♯‘∅)) ≠ ∅ ↔ (♯‘∅) ∈ ℕ)
36	34, 35	mtbir 326	. . . . 5 ⊢ ¬ (0..^(♯‘∅)) ≠ ∅
37		nne 2961	. . . . 5 ⊢ (¬ (0..^(♯‘∅)) ≠ ∅ ↔ (0..^(♯‘∅)) = ∅)
38	36, 37	mpbi 233	. . . 4 ⊢ (0..^(♯‘∅)) = ∅
39		rzal 4453	. . . 4 ⊢ ((0..^(♯‘∅)) = ∅ → ∀𝑖 ∈ (0..^(♯‘∅))(∅‘𝑖) ∼ (lastS‘∅))
40	38, 39	mp1i 14	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘∅))(∅‘𝑖) ∼ (lastS‘∅))
41		chner.1	. . . . . . . 8 ⊢ (𝜑 → ∼ Er 𝐴)
42	41	ad6antr 749	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → ∼ Er 𝐴)
43		simp-5r 798	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑥 ∈ 𝐴)
44	42, 43	erref 8721	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑥 ∼ 𝑥)
45		simp-6r 800	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑑 ∈ ( ∼ Chain 𝐴))
46	45	chnwrd 18702	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑑 ∈ Word 𝐴)
47		simplr 781	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))))
48		ccatws1len 14692	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
49	46, 48	syl 18	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
50		fveq2 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
51	50, 32	eqtr2di 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = ∅ → 0 = (♯‘𝑑))
52	51	eqcomd 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = ∅ → (♯‘𝑑) = 0)
53	52	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → (♯‘𝑑) = 0)
54	53	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → ((♯‘𝑑) + 1) = (0 + 1))
55		0p1e1 12389	. . . . . . . . . . . . . 14 ⊢ (0 + 1) = 1
56	54, 55	eqtrdi 2813	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → ((♯‘𝑑) + 1) = 1)
57	49, 56	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = 1)
58	57	oveq2d 7433	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))) = (0..^1))
59	47, 58	eleqtrd 2864	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑗 ∈ (0..^1))
60		fzo01 13807	. . . . . . . . . 10 ⊢ (0..^1) = {0}
61	59, 60	eleqtrdi 2872	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑗 ∈ {0})
62	61	elsnd 4605	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑗 = 0)
63	51	adantl 487	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 0 = (♯‘𝑑))
64	62, 63	eqtrd 2797	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → 𝑗 = (♯‘𝑑))
65		ccats1val2 14699	. . . . . . 7 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑗 = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = 𝑥)
66	46, 43, 64, 65	syl3anc 1398	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = 𝑥)
67		lswccats1 14706	. . . . . . 7 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑥 ∈ 𝐴) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
68	46, 43, 67	syl2anc 596	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
69	44, 66, 68	3brtr4d 5141	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 = ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
70	41	ad6antr 749	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → ∼ Er 𝐴)
71		simp-6r 800	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → 𝑑 ∈ ( ∼ Chain 𝐴))
72	71	chnwrd 18702	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → 𝑑 ∈ Word 𝐴)
73	72	adantr 486	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = (♯‘𝑑)) → 𝑑 ∈ Word 𝐴)
74		simp-6r 800	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = (♯‘𝑑)) → 𝑥 ∈ 𝐴)
75		simpr 490	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = (♯‘𝑑)) → 𝑗 = (♯‘𝑑))
76	73, 74, 75, 65	syl3anc 1398	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) = 𝑥)
77		simp-4r 796	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥))
78		neneq 2963	. . . . . . . . . . . . 13 ⊢ (𝑑 ≠ ∅ → ¬ 𝑑 = ∅)
79	78	adantl 487	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → ¬ 𝑑 = ∅)
80	77, 79	orcnd 892	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → (lastS‘𝑑) ∼ 𝑥)
81	70, 80	ersym 8713	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → 𝑥 ∼ (lastS‘𝑑))
82	81	adantr 486	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = (♯‘𝑑)) → 𝑥 ∼ (lastS‘𝑑))
83	76, 82	eqbrtrd 5131	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 = (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘𝑑))
84		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗))
85	84	breq1d 5117	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ∼ (lastS‘𝑑) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘𝑑)))
86		simp-4r 796	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑))
87		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → 𝑑 ∈ ( ∼ Chain 𝐴))
88	87	chnwrd 18702	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → 𝑑 ∈ Word 𝐴)
89		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → 𝑖 ∈ (0..^(♯‘𝑑)))
90		ccats1val1 14698	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ Word 𝐴 ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = (𝑑‘𝑖))
91	88, 89, 90	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) = (𝑑‘𝑖))
92	91	eqcomd 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → (𝑑‘𝑖) = ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖))
93	92	breq1d 5117	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑖 ∈ (0..^(♯‘𝑑))) → ((𝑑‘𝑖) ∼ (lastS‘𝑑) ↔ ((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ∼ (lastS‘𝑑)))
94	93	ralbidva 3185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) → (∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑) ↔ ∀𝑖 ∈ (0..^(♯‘𝑑))((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ∼ (lastS‘𝑑)))
95	94	ad6antr 749	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → (∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑) ↔ ∀𝑖 ∈ (0..^(♯‘𝑑))((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ∼ (lastS‘𝑑)))
96	86, 95	mpbid 235	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → ∀𝑖 ∈ (0..^(♯‘𝑑))((𝑑 ++ ⟨“𝑥”⟩)‘𝑖) ∼ (lastS‘𝑑))
97		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))))
98		simp-5r 798	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → 𝑑 ∈ ( ∼ Chain 𝐴))
99	98	chnwrd 18702	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → 𝑑 ∈ Word 𝐴)
100	99, 48	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → (♯‘(𝑑 ++ ⟨“𝑥”⟩)) = ((♯‘𝑑) + 1))
101	100	oveq2d 7433	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩))) = (0..^((♯‘𝑑) + 1)))
102	97, 101	eleqtrd 2864	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → 𝑗 ∈ (0..^((♯‘𝑑) + 1)))
103	102	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → 𝑗 ∈ (0..^((♯‘𝑑) + 1)))
104		simp-7r 802	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → 𝑑 ∈ ( ∼ Chain 𝐴))
105	104	chnwrd 18702	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → 𝑑 ∈ Word 𝐴)
106		lencl 14602	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ Word 𝐴 → (♯‘𝑑) ∈ ℕ₀)
107		elnn0uz 12932	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑑) ∈ ℕ₀ ↔ (♯‘𝑑) ∈ (ℤ_≥‘0))
108	107	biimpi 219	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑑) ∈ ℕ₀ → (♯‘𝑑) ∈ (ℤ_≥‘0))
109	105, 106, 108	3syl 19	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → (♯‘𝑑) ∈ (ℤ_≥‘0))
110		fzosplitsni 13839	. . . . . . . . . . . 12 ⊢ ((♯‘𝑑) ∈ (ℤ_≥‘0) → (𝑗 ∈ (0..^((♯‘𝑑) + 1)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∨ 𝑗 = (♯‘𝑑))))
111	109, 110	syl 18	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → (𝑗 ∈ (0..^((♯‘𝑑) + 1)) ↔ (𝑗 ∈ (0..^(♯‘𝑑)) ∨ 𝑗 = (♯‘𝑑))))
112	103, 111	mpbid 235	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → (𝑗 ∈ (0..^(♯‘𝑑)) ∨ 𝑗 = (♯‘𝑑)))
113		df-ne 2958	. . . . . . . . . . 11 ⊢ (𝑗 ≠ (♯‘𝑑) ↔ ¬ 𝑗 = (♯‘𝑑))
114	113	bilani 510	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → ¬ 𝑗 = (♯‘𝑑))
115	112, 114	olcnd 891	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → 𝑗 ∈ (0..^(♯‘𝑑)))
116	85, 96, 115	rspcdva 3580	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) ∧ 𝑗 ≠ (♯‘𝑑)) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘𝑑))
117	83, 116	pm2.61dane 3044	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘𝑑))
118	70, 117, 80	ertrd 8717	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ 𝑥)
119		simp-5r 798	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → 𝑥 ∈ 𝐴)
120	72, 119, 67	syl2anc 596	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → (lastS‘(𝑑 ++ ⟨“𝑥”⟩)) = 𝑥)
121	118, 120	breqtrrd 5137	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) ∧ 𝑑 ≠ ∅) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
122	69, 121	pm2.61dane 3044	. . . 4 ⊢ ((((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) ∧ 𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))) → ((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
123	122	ralrimiva 3156	. . 3 ⊢ (((((𝜑 ∧ 𝑑 ∈ ( ∼ Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) ∼ 𝑥)) ∧ ∀𝑖 ∈ (0..^(♯‘𝑑))(𝑑‘𝑖) ∼ (lastS‘𝑑)) → ∀𝑗 ∈ (0..^(♯‘(𝑑 ++ ⟨“𝑥”⟩)))((𝑑 ++ ⟨“𝑥”⟩)‘𝑗) ∼ (lastS‘(𝑑 ++ ⟨“𝑥”⟩)))
124	8, 14, 24, 30, 31, 40, 123	chnind 18715	. 2 ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) ∼ (lastS‘𝐶))
125		chner.3	. 2 ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))
126	2, 124, 125	rspcdva 3580	1 ⊢ (𝜑 → (𝐶‘𝐽) ∼ (lastS‘𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∅c0 4282 {csn 4587 class class class wbr 5107 ‘cfv 6537 (class class class)co 7417 Er wer 8697 0cc0 11128 1c1 11129 + caddc 11131 ℕcn 12261 ℕ₀cn0 12532 ℤ_≥cuz 12891 ..^cfzo 13713 ♯chash 14398 Word cword 14582 lastSclsw 14631 ++ cconcat 14639 ⟨“cs1 14666 Chain cchn 18699

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-n0 12533 df-xnn0 12606 df-z 12620 df-uz 12892 df-rp 13047 df-fz 13566 df-fzo 13714 df-hash 14399 df-word 14583 df-lsw 14632 df-concat 14640 df-s1 14667 df-substr 14713 df-pfx 14745 df-chn 18700

This theorem is used by: chnerlem2 47719

W3C validator