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 32930

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 6763	. . . . . . . . . . . . 13 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
4	2, 3	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇:(0..^𝑁)⟶(0..^𝑁))
5		iswrdi 14424	. . . . . . . . . . . 12 ⊢ (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6		lencl 14440	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ₀)
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) ∈ ℕ₀)
8	1, 7	eqeltrid 2835	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
9		fzossfzop1 13643	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11		ccatws1f1o.2	. . . . . . . . 9 ⊢ 𝐽 = (0..^(𝑁 + 1))
12	10, 11	sseqtrrdi 3976	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) ⊆ 𝐽)
13	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
14	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
15	1	eqcomi 2740	. . . . . . . . . . . 12 ⊢ (♯‘𝑇) = 𝑁
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) = 𝑁)
17	16	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
18	17	eleq2d 2817	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
19	18	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
20	14, 19	ffvelcdmd 7018	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ (0..^𝑁))
21	13, 20	sseldd 3935	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
22	21	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
23	11	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 = (0..^(𝑁 + 1)))
24		fzo0ssnn0 13646	. . . . . . . . . . . . 13 ⊢ (0..^(𝑁 + 1)) ⊆ ℕ₀
25	23, 24	eqsstrdi 3979	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ ℕ₀)
26	25	sselda 3934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ₀)
27	26	nn0cnd 12444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℂ)
28	27	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29		nn0uz 12774	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
30	8, 29	eleqtrdi 2841	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
31	30	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ_≥‘0))
32	23	eleq2d 2817	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ (0..^(𝑁 + 1))))
33	32	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
34	33	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35		fzosplitsni 13679	. . . . . . . . . . . . 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 878	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = 𝑁)
42	41, 1	eqtrdi 2782	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
43	28, 42	subeq0bd 11543	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
44	43	fveq2d 6826	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45		s1fv 14518	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (⟨“𝑁”⟩‘0) = 𝑁)
46	8, 45	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
47	46	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
48	44, 47	eqtrd 2766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49		fzonn0p1 13642	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0..^(𝑁 + 1)))
50	8, 49	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(𝑁 + 1)))
51	50, 11	eleqtrrdi 2842	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ 𝐽)
52	51	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ 𝐽)
53	48, 52	eqeltrd 2831	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
54	22, 53	ifclda 4511	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
55	54	ralrimiva 3124	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
56	12	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ 𝐽)
57		f1ocnv 6775	. . . . . . . . . 10 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → ^◡𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
58		f1of 6763	. . . . . . . . . 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 7017	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^𝑁))
62	56, 61	sseldd 3935	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ 𝐽)
63	1	oveq2i 7357	. . . . . . . . 9 ⊢ (0..^𝑁) = (0..^(♯‘𝑇))
64	61, 63	eleqtrdi 2841	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)))
65	64	iftrued 4483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) = (𝑇‘(^◡𝑇‘𝑦)))
66	2	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68		f1ocnvfv2 7211	. . . . . . . 8 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
69	66, 67, 68	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
70	65, 69	eqtr2d 2767	. . . . . 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 757	. . . . . . . . . . . . . 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 13573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 𝑁 ∈ (0..^𝑁)
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
80	63	eleq2i 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
81	79, 80	sylnib 328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
82	77, 81	eqneltrd 2851	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
83	82	iffalsed 4486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
84	11, 24	eqsstri 3981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 ⊆ ℕ₀
85		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ 𝐽)
86	84, 85	sselid 3932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ₀)
87	86	nn0cnd 12444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
88	77, 1	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
89	87, 88	subeq0bd 11543	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
90	89	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
91	46	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
92	90, 91	eqtrd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
93	76, 83, 92	3eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
94	93, 79	eqneltrd 2851	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑦 ∈ (0..^𝑁))
95	75, 94	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 = 𝑁)
96	74, 95	olcnd 877	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^𝑁))
97	96, 63	eleqtrdi 2841	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
98	97	iftrued 4483	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
99	71, 98	eqtrd 2766	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇‘𝑥))
100	99	fveq2d 6826	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘𝑦) = (^◡𝑇‘(𝑇‘𝑥)))
101	66	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102		f1ocnvfv1 7210	. . . . . . . . . 10 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
103	101, 96, 102	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
104	100, 103	eqtr2d 2767	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (^◡𝑇‘𝑦))
105	104	ex 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
106	105	ralrimiva 3124	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
107		eleq1 2819	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇))))
108		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑇‘𝑥) = (𝑇‘(^◡𝑇‘𝑦)))
109		fvoveq1 7369	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))
110	107, 108, 109	ifbieq12d 4504	. . . . . . . 8 ⊢ (𝑥 = (^◡𝑇‘𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
111	110	eqeq2d 2742	. . . . . . 7 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))))
112	111	eqreu 3688	. . . . . 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 12444	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
116	115	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
117	1	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118	116, 117	subeq0bd 11543	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119	118	fveq2d 6826	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
120	46	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121	119, 120	eqtrd 2766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
122	78	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123	122, 80	sylnib 328	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124	123	iffalsed 4486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126	121, 124, 125	3eqtr4rd 2777	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
127	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑁 ∈ (ℤ_≥‘0))
128	127	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑁 ∈ (ℤ_≥‘0))
129	33	ad5ant14 757	. . . . . . . . . 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 775	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = 𝑁)
133	131, 132	eqtr3d 2768	. . . . . . . . . . . 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 2817	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137	136	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138	137	iftrued 4483	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
139	4	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140	139	ffvelcdmda 7017	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘𝑥) ∈ (0..^𝑁))
141	138, 140	eqeltrd 2831	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142	134, 141	eqeltrrd 2832	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑁 ∈ (0..^𝑁))
143	78	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → ¬ 𝑁 ∈ (0..^𝑁))
144	142, 143	pm2.65da 816	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 ∈ (0..^𝑁))
145	130, 144	orcnd 878	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = 𝑁)
146	145	ex 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
147	146	ralrimiva 3124	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148		eleq1 2819	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑇‘𝑥) = (𝑇‘𝑁))
150		fvoveq1 7369	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151	148, 149, 150	ifbieq12d 4504	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152	151	eqeq2d 2742	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153	152	eqreu 3688	. . . . . 6 ⊢ ((𝑁 ∈ 𝐽 ∧ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154	114, 126, 147, 153	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
155	23	eleq2d 2817	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (0..^(𝑁 + 1))))
156	155	biimpa 476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157		fzosplitsni 13679	. . . . . . 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 960	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
161	160	ralrimiva 3124	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162		s1len 14514	. . . . . . . 8 ⊢ (♯‘⟨“𝑁”⟩) = 1
163	15, 162	oveq12i 7358	. . . . . . 7 ⊢ ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164	163	oveq2i 7357	. . . . . 6 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165	164, 11	eqtr4i 2757	. . . . 5 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166	165	mpteq1i 5182	. . . 4 ⊢ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥 ∈ 𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167	166	f1ompt 7044	. . 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 7379	. . . . 5 ⊢ (0..^𝑁) ∈ V
170		fex 7160	. . . . 5 ⊢ ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
171	4, 169, 170	sylancl 586	. . . 4 ⊢ (𝜑 → 𝑇 ∈ V)
172		s1cli 14513	. . . 4 ⊢ ⟨“𝑁”⟩ ∈ Word V
173		ccatfval 14480	. . . 4 ⊢ ((𝑇 ∈ V ∧ ⟨“𝑁”⟩ ∈ Word V) → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
174	171, 172, 173	sylancl 586	. . 3 ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
175	174	f1oeq1d 6758	. 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 847 = wceq 1541 ∈ wcel 2111 ∀wral 3047 ∃!wreu 3344 Vcvv 3436 ⊆ wss 3902 ifcif 4475 ↦ cmpt 5172 ^◡ccnv 5615 ⟶wf 6477 –1-1-onto→wf1o 6480 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 0cc0 11006 1c1 11007 + caddc 11009 − cmin 11344 ℕ₀cn0 12381 ℤ_≥cuz 12732 ..^cfzo 13554 ♯chash 14237 Word cword 14420 ++ cconcat 14477 ⟨“cs1 14503

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-n0 12382 df-z 12469 df-uz 12733 df-fz 13408 df-fzo 13555 df-hash 14238 df-word 14421 df-concat 14478 df-s1 14504

This theorem is referenced by: 1arithidomlem2 33499

W3C validator