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 32939

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 6768	. . . . . . . . . . . . 13 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
4	2, 3	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇:(0..^𝑁)⟶(0..^𝑁))
5		iswrdi 14426	. . . . . . . . . . . 12 ⊢ (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6		lencl 14442	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ₀)
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) ∈ ℕ₀)
8	1, 7	eqeltrid 2837	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
9		fzossfzop1 13645	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11		ccatws1f1o.2	. . . . . . . . 9 ⊢ 𝐽 = (0..^(𝑁 + 1))
12	10, 11	sseqtrrdi 3972	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) ⊆ 𝐽)
13	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
14	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
15	1	eqcomi 2742	. . . . . . . . . . . 12 ⊢ (♯‘𝑇) = 𝑁
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) = 𝑁)
17	16	oveq2d 7368	. . . . . . . . . 10 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
18	17	eleq2d 2819	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
19	18	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
20	14, 19	ffvelcdmd 7024	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ (0..^𝑁))
21	13, 20	sseldd 3931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
22	21	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
23	11	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 = (0..^(𝑁 + 1)))
24		fzo0ssnn0 13648	. . . . . . . . . . . . 13 ⊢ (0..^(𝑁 + 1)) ⊆ ℕ₀
25	23, 24	eqsstrdi 3975	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ ℕ₀)
26	25	sselda 3930	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ₀)
27	26	nn0cnd 12451	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℂ)
28	27	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29		nn0uz 12776	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
30	8, 29	eleqtrdi 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
31	30	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ_≥‘0))
32	23	eleq2d 2819	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ (0..^(𝑁 + 1))))
33	32	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
34	33	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35		fzosplitsni 13681	. . . . . . . . . . . . 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 2784	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
43	28, 42	subeq0bd 11550	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
44	43	fveq2d 6832	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45		s1fv 14520	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (⟨“𝑁”⟩‘0) = 𝑁)
46	8, 45	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
47	46	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
48	44, 47	eqtrd 2768	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49		fzonn0p1 13644	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0..^(𝑁 + 1)))
50	8, 49	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(𝑁 + 1)))
51	50, 11	eleqtrrdi 2844	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ 𝐽)
52	51	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ 𝐽)
53	48, 52	eqeltrd 2833	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
54	22, 53	ifclda 4510	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
55	54	ralrimiva 3125	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
56	12	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ 𝐽)
57		f1ocnv 6780	. . . . . . . . . 10 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → ^◡𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
58		f1of 6768	. . . . . . . . . 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 7023	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^𝑁))
62	56, 61	sseldd 3931	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ 𝐽)
63	1	oveq2i 7363	. . . . . . . . 9 ⊢ (0..^𝑁) = (0..^(♯‘𝑇))
64	61, 63	eleqtrdi 2843	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)))
65	64	iftrued 4482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) = (𝑇‘(^◡𝑇‘𝑦)))
66	2	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68		f1ocnvfv2 7217	. . . . . . . 8 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
69	66, 67, 68	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
70	65, 69	eqtr2d 2769	. . . . . 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 13575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 𝑁 ∈ (0..^𝑁)
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
80	63	eleq2i 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
81	79, 80	sylnib 328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
82	77, 81	eqneltrd 2853	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
83	82	iffalsed 4485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
84	11, 24	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 ⊆ ℕ₀
85		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ 𝐽)
86	84, 85	sselid 3928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ₀)
87	86	nn0cnd 12451	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
88	77, 1	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
89	87, 88	subeq0bd 11550	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
90	89	fveq2d 6832	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
91	46	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
92	90, 91	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
93	76, 83, 92	3eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
94	93, 79	eqneltrd 2853	. . . . . . . . . . . . . . 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 2843	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
98	97	iftrued 4482	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
99	71, 98	eqtrd 2768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇‘𝑥))
100	99	fveq2d 6832	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘𝑦) = (^◡𝑇‘(𝑇‘𝑥)))
101	66	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102		f1ocnvfv1 7216	. . . . . . . . . 10 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
103	101, 96, 102	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
104	100, 103	eqtr2d 2769	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (^◡𝑇‘𝑦))
105	104	ex 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
106	105	ralrimiva 3125	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
107		eleq1 2821	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇))))
108		fveq2 6828	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑇‘𝑥) = (𝑇‘(^◡𝑇‘𝑦)))
109		fvoveq1 7375	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))
110	107, 108, 109	ifbieq12d 4503	. . . . . . . 8 ⊢ (𝑥 = (^◡𝑇‘𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
111	110	eqeq2d 2744	. . . . . . 7 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))))
112	111	eqreu 3684	. . . . . 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 12451	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
116	115	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
117	1	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118	116, 117	subeq0bd 11550	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119	118	fveq2d 6832	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
120	46	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121	119, 120	eqtrd 2768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
122	78	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123	122, 80	sylnib 328	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124	123	iffalsed 4485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126	121, 124, 125	3eqtr4rd 2779	. . . . . 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 2770	. . . . . . . . . . . 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 2819	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137	136	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138	137	iftrued 4482	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
139	4	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140	139	ffvelcdmda 7023	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘𝑥) ∈ (0..^𝑁))
141	138, 140	eqeltrd 2833	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142	134, 141	eqeltrrd 2834	. . . . . . . . . 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 3125	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148		eleq1 2821	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149		fveq2 6828	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑇‘𝑥) = (𝑇‘𝑁))
150		fvoveq1 7375	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151	148, 149, 150	ifbieq12d 4503	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152	151	eqeq2d 2744	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153	152	eqreu 3684	. . . . . 6 ⊢ ((𝑁 ∈ 𝐽 ∧ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154	114, 126, 147, 153	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
155	23	eleq2d 2819	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (0..^(𝑁 + 1))))
156	155	biimpa 476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157		fzosplitsni 13681	. . . . . . 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 3125	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162		s1len 14516	. . . . . . . 8 ⊢ (♯‘⟨“𝑁”⟩) = 1
163	15, 162	oveq12i 7364	. . . . . . 7 ⊢ ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164	163	oveq2i 7363	. . . . . 6 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165	164, 11	eqtr4i 2759	. . . . 5 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166	165	mpteq1i 5184	. . . 4 ⊢ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥 ∈ 𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167	166	f1ompt 7050	. . 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 7385	. . . . 5 ⊢ (0..^𝑁) ∈ V
170		fex 7166	. . . . 5 ⊢ ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
171	4, 169, 170	sylancl 586	. . . 4 ⊢ (𝜑 → 𝑇 ∈ V)
172		s1cli 14515	. . . 4 ⊢ ⟨“𝑁”⟩ ∈ Word V
173		ccatfval 14482	. . . 4 ⊢ ((𝑇 ∈ V ∧ ⟨“𝑁”⟩ ∈ Word V) → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
174	171, 172, 173	sylancl 586	. . 3 ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
175	174	f1oeq1d 6763	. 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 2113 ∀wral 3048 ∃!wreu 3345 Vcvv 3437 ⊆ wss 3898 ifcif 4474 ↦ cmpt 5174 ^◡ccnv 5618 ⟶wf 6482 –1-1-onto→wf1o 6485 ‘cfv 6486 (class class class)co 7352 ℂcc 11011 0cc0 11013 1c1 11014 + caddc 11016 − cmin 11351 ℕ₀cn0 12388 ℤ_≥cuz 12738 ..^cfzo 13556 ♯chash 14239 Word cword 14422 ++ cconcat 14479 ⟨“cs1 14505

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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090

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 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-card 9839 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-nn 12133 df-n0 12389 df-z 12476 df-uz 12739 df-fz 13410 df-fzo 13557 df-hash 14240 df-word 14423 df-concat 14480 df-s1 14506

This theorem is referenced by: 1arithidomlem2 33508

W3C validator