ccatws1f1o - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ccatws1f1o		Structured version Visualization version GIF version

Theorem ccatws1f1o 32936

Description: Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025.)

**Hypotheses**
Ref	Expression
ccatws1f1o.1	⊢ 𝑁 = (♯‘𝑇)
ccatws1f1o.2	⊢ 𝐽 = (0..^(𝑁 + 1))
ccatws1f1o.3	⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))

**Assertion**
Ref	Expression
ccatws1f1o	⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽)

Proof of Theorem ccatws1f1o Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ccatws1f1o.1	. . . . . . . . . . 11 ⊢ 𝑁 = (♯‘𝑇)
2		ccatws1f1o.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
3		f1of 6848	. . . . . . . . . . . . 13 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
4	2, 3	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇:(0..^𝑁)⟶(0..^𝑁))
5		iswrdi 14556	. . . . . . . . . . . 12 ⊢ (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6		lencl 14571	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ₀)
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) ∈ ℕ₀)
8	1, 7	eqeltrid 2845	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
9		fzossfzop1 13782	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11		ccatws1f1o.2	. . . . . . . . 9 ⊢ 𝐽 = (0..^(𝑁 + 1))
12	10, 11	sseqtrrdi 4025	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) ⊆ 𝐽)
13	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
14	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
15	1	eqcomi 2746	. . . . . . . . . . . 12 ⊢ (♯‘𝑇) = 𝑁
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) = 𝑁)
17	16	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
18	17	eleq2d 2827	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
19	18	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
20	14, 19	ffvelcdmd 7105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ (0..^𝑁))
21	13, 20	sseldd 3984	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
22	21	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
23	11	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 = (0..^(𝑁 + 1)))
24		fzo0ssnn0 13785	. . . . . . . . . . . . 13 ⊢ (0..^(𝑁 + 1)) ⊆ ℕ₀
25	23, 24	eqsstrdi 4028	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ ℕ₀)
26	25	sselda 3983	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ₀)
27	26	nn0cnd 12589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℂ)
28	27	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29		nn0uz 12920	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
30	8, 29	eleqtrdi 2851	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
31	30	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ_≥‘0))
32	23	eleq2d 2827	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ (0..^(𝑁 + 1))))
33	32	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
34	33	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35		fzosplitsni 13817	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (𝑥 ∈ (0..^(𝑁 + 1)) ↔ (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁)))
36	35	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘0) ∧ 𝑥 ∈ (0..^(𝑁 + 1))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
37	31, 34, 36	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
38	18	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ 𝑥 ∈ (0..^(♯‘𝑇)) ↔ ¬ 𝑥 ∈ (0..^𝑁)))
39	38	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → ¬ 𝑥 ∈ (0..^𝑁))
40	39	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → ¬ 𝑥 ∈ (0..^𝑁))
41	37, 40	orcnd 879	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = 𝑁)
42	41, 1	eqtrdi 2793	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
43	28, 42	subeq0bd 11689	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
44	43	fveq2d 6910	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45		s1fv 14648	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (⟨“𝑁”⟩‘0) = 𝑁)
46	8, 45	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
47	46	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
48	44, 47	eqtrd 2777	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49		fzonn0p1 13781	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0..^(𝑁 + 1)))
50	8, 49	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(𝑁 + 1)))
51	50, 11	eleqtrrdi 2852	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ 𝐽)
52	51	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ 𝐽)
53	48, 52	eqeltrd 2841	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
54	22, 53	ifclda 4561	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
55	54	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
56	12	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ 𝐽)
57		f1ocnv 6860	. . . . . . . . . 10 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → ^◡𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
58		f1of 6848	. . . . . . . . . 10 ⊢ (^◡𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → ^◡𝑇:(0..^𝑁)⟶(0..^𝑁))
59	2, 57, 58	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝑇:(0..^𝑁)⟶(0..^𝑁))
60	59	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ^◡𝑇:(0..^𝑁)⟶(0..^𝑁))
61	60	ffvelcdmda 7104	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^𝑁))
62	56, 61	sseldd 3984	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ 𝐽)
63	1	oveq2i 7442	. . . . . . . . 9 ⊢ (0..^𝑁) = (0..^(♯‘𝑇))
64	61, 63	eleqtrdi 2851	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)))
65	64	iftrued 4533	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) = (𝑇‘(^◡𝑇‘𝑦)))
66	2	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68		f1ocnvfv2 7297	. . . . . . . 8 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
69	66, 67, 68	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
70	65, 69	eqtr2d 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
71		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
72	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑁 ∈ (ℤ_≥‘0))
73	72, 33, 36	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
74	73	ad5ant14 758	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
75	67	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 ∈ (0..^𝑁))
76	71	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
77		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = 𝑁)
78		fzonel 13713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 𝑁 ∈ (0..^𝑁)
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
80	63	eleq2i 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
81	79, 80	sylnib 328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
82	77, 81	eqneltrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
83	82	iffalsed 4536	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
84	11, 24	eqsstri 4030	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 ⊆ ℕ₀
85		simpllr 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ 𝐽)
86	84, 85	sselid 3981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ₀)
87	86	nn0cnd 12589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
88	77, 1	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
89	87, 88	subeq0bd 11689	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
90	89	fveq2d 6910	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
91	46	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
92	90, 91	eqtrd 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
93	76, 83, 92	3eqtrd 2781	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
94	93, 79	eqneltrd 2861	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑦 ∈ (0..^𝑁))
95	75, 94	pm2.65da 817	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 = 𝑁)
96	74, 95	olcnd 878	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^𝑁))
97	96, 63	eleqtrdi 2851	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
98	97	iftrued 4533	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
99	71, 98	eqtrd 2777	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇‘𝑥))
100	99	fveq2d 6910	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘𝑦) = (^◡𝑇‘(𝑇‘𝑥)))
101	66	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102		f1ocnvfv1 7296	. . . . . . . . . 10 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
103	101, 96, 102	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
104	100, 103	eqtr2d 2778	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (^◡𝑇‘𝑦))
105	104	ex 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
106	105	ralrimiva 3146	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
107		eleq1 2829	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇))))
108		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑇‘𝑥) = (𝑇‘(^◡𝑇‘𝑦)))
109		fvoveq1 7454	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))
110	107, 108, 109	ifbieq12d 4554	. . . . . . . 8 ⊢ (𝑥 = (^◡𝑇‘𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
111	110	eqeq2d 2748	. . . . . . 7 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))))
112	111	eqreu 3735	. . . . . 6 ⊢ (((^◡𝑇‘𝑦) ∈ 𝐽 ∧ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦))) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
113	62, 70, 106, 112	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
114	51	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ 𝐽)
115	8	nn0cnd 12589	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
116	115	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
117	1	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118	116, 117	subeq0bd 11689	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119	118	fveq2d 6910	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
120	46	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121	119, 120	eqtrd 2777	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
122	78	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123	122, 80	sylnib 328	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124	123	iffalsed 4536	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126	121, 124, 125	3eqtr4rd 2788	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
127	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑁 ∈ (ℤ_≥‘0))
128	127	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑁 ∈ (ℤ_≥‘0))
129	33	ad5ant14 758	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(𝑁 + 1)))
130	128, 129, 36	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
131		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
132		simpllr 776	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = 𝑁)
133	131, 132	eqtr3d 2779	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
134	133	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
135	63	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (0..^𝑁) = (0..^(♯‘𝑇)))
136	135	eleq2d 2827	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137	136	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138	137	iftrued 4533	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
139	4	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140	139	ffvelcdmda 7104	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘𝑥) ∈ (0..^𝑁))
141	138, 140	eqeltrd 2841	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142	134, 141	eqeltrrd 2842	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑁 ∈ (0..^𝑁))
143	78	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → ¬ 𝑁 ∈ (0..^𝑁))
144	142, 143	pm2.65da 817	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 ∈ (0..^𝑁))
145	130, 144	orcnd 879	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = 𝑁)
146	145	ex 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
147	146	ralrimiva 3146	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148		eleq1 2829	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑇‘𝑥) = (𝑇‘𝑁))
150		fvoveq1 7454	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151	148, 149, 150	ifbieq12d 4554	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152	151	eqeq2d 2748	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153	152	eqreu 3735	. . . . . 6 ⊢ ((𝑁 ∈ 𝐽 ∧ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154	114, 126, 147, 153	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
155	23	eleq2d 2827	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (0..^(𝑁 + 1))))
156	155	biimpa 476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157		fzosplitsni 13817	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (𝑦 ∈ (0..^(𝑁 + 1)) ↔ (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁)))
158	157	biimpa 476	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘0) ∧ 𝑦 ∈ (0..^(𝑁 + 1))) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
159	127, 156, 158	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
160	113, 154, 159	mpjaodan 961	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
161	160	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162		s1len 14644	. . . . . . . 8 ⊢ (♯‘⟨“𝑁”⟩) = 1
163	15, 162	oveq12i 7443	. . . . . . 7 ⊢ ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164	163	oveq2i 7442	. . . . . 6 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165	164, 11	eqtr4i 2768	. . . . 5 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166	165	mpteq1i 5238	. . . 4 ⊢ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥 ∈ 𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167	166	f1ompt 7131	. . 3 ⊢ ((𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽–1-1-onto→𝐽 ↔ (∀𝑥 ∈ 𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽 ∧ ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
168	55, 161, 167	sylanbrc 583	. 2 ⊢ (𝜑 → (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽–1-1-onto→𝐽)
169		ovex 7464	. . . . 5 ⊢ (0..^𝑁) ∈ V
170		fex 7246	. . . . 5 ⊢ ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
171	4, 169, 170	sylancl 586	. . . 4 ⊢ (𝜑 → 𝑇 ∈ V)
172		s1cli 14643	. . . 4 ⊢ ⟨“𝑁”⟩ ∈ Word V
173		ccatfval 14611	. . . 4 ⊢ ((𝑇 ∈ V ∧ ⟨“𝑁”⟩ ∈ Word V) → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
174	171, 172, 173	sylancl 586	. . 3 ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
175	174	f1oeq1d 6843	. 2 ⊢ (𝜑 → ((𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽 ↔ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽–1-1-onto→𝐽))
176	168, 175	mpbird 257	1 ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃!wreu 3378 Vcvv 3480 ⊆ wss 3951 ifcif 4525 ↦ cmpt 5225 ^◡ccnv 5684 ⟶wf 6557 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 0cc0 11155 1c1 11156 + caddc 11158 − cmin 11492 ℕ₀cn0 12526 ℤ_≥cuz 12878 ..^cfzo 13694 ♯chash 14369 Word cword 14552 ++ cconcat 14608 ⟨“cs1 14633

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-z 12614 df-uz 12879 df-fz 13548 df-fzo 13695 df-hash 14370 df-word 14553 df-concat 14609 df-s1 14634

This theorem is referenced by: 1arithidomlem2 33564

W3C validator