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 32906

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 14442	. . . . . . . . . . . 12 ⊢ (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6		lencl 14458	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ₀)
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) ∈ ℕ₀)
8	1, 7	eqeltrid 2832	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
9		fzossfzop1 13664	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11		ccatws1f1o.2	. . . . . . . . 9 ⊢ 𝐽 = (0..^(𝑁 + 1))
12	10, 11	sseqtrrdi 3979	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) ⊆ 𝐽)
13	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
14	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
15	1	eqcomi 2738	. . . . . . . . . . . 12 ⊢ (♯‘𝑇) = 𝑁
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) = 𝑁)
17	16	oveq2d 7369	. . . . . . . . . 10 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
18	17	eleq2d 2814	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
19	18	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
20	14, 19	ffvelcdmd 7023	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ (0..^𝑁))
21	13, 20	sseldd 3938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
22	21	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
23	11	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 = (0..^(𝑁 + 1)))
24		fzo0ssnn0 13667	. . . . . . . . . . . . 13 ⊢ (0..^(𝑁 + 1)) ⊆ ℕ₀
25	23, 24	eqsstrdi 3982	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ ℕ₀)
26	25	sselda 3937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ₀)
27	26	nn0cnd 12465	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℂ)
28	27	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29		nn0uz 12795	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
30	8, 29	eleqtrdi 2838	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
31	30	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ_≥‘0))
32	23	eleq2d 2814	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ (0..^(𝑁 + 1))))
33	32	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
34	33	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35		fzosplitsni 13699	. . . . . . . . . . . . 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 2780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
43	28, 42	subeq0bd 11564	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
44	43	fveq2d 6830	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45		s1fv 14535	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (⟨“𝑁”⟩‘0) = 𝑁)
46	8, 45	syl 17	. . . . . . . 8 ⊢ (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
47	46	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
48	44, 47	eqtrd 2764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49		fzonn0p1 13663	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0..^(𝑁 + 1)))
50	8, 49	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(𝑁 + 1)))
51	50, 11	eleqtrrdi 2839	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ 𝐽)
52	51	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ 𝐽)
53	48, 52	eqeltrd 2828	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
54	22, 53	ifclda 4514	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
55	54	ralrimiva 3121	. . 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 7022	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^𝑁))
62	56, 61	sseldd 3938	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ 𝐽)
63	1	oveq2i 7364	. . . . . . . . 9 ⊢ (0..^𝑁) = (0..^(♯‘𝑇))
64	61, 63	eleqtrdi 2838	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)))
65	64	iftrued 4486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) = (𝑇‘(^◡𝑇‘𝑦)))
66	2	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68		f1ocnvfv2 7218	. . . . . . . 8 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
69	66, 67, 68	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
70	65, 69	eqtr2d 2765	. . . . . 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 13594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 𝑁 ∈ (0..^𝑁)
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
80	63	eleq2i 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
81	79, 80	sylnib 328	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
82	77, 81	eqneltrd 2848	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
83	82	iffalsed 4489	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
84	11, 24	eqsstri 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 ⊆ ℕ₀
85		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ 𝐽)
86	84, 85	sselid 3935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ₀)
87	86	nn0cnd 12465	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
88	77, 1	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
89	87, 88	subeq0bd 11564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
90	89	fveq2d 6830	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
91	46	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
92	90, 91	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
93	76, 83, 92	3eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
94	93, 79	eqneltrd 2848	. . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
98	97	iftrued 4486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
99	71, 98	eqtrd 2764	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇‘𝑥))
100	99	fveq2d 6830	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘𝑦) = (^◡𝑇‘(𝑇‘𝑥)))
101	66	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102		f1ocnvfv1 7217	. . . . . . . . . 10 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
103	101, 96, 102	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
104	100, 103	eqtr2d 2765	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (^◡𝑇‘𝑦))
105	104	ex 412	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
106	105	ralrimiva 3121	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
107		eleq1 2816	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇))))
108		fveq2 6826	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑇‘𝑥) = (𝑇‘(^◡𝑇‘𝑦)))
109		fvoveq1 7376	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))
110	107, 108, 109	ifbieq12d 4507	. . . . . . . 8 ⊢ (𝑥 = (^◡𝑇‘𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
111	110	eqeq2d 2740	. . . . . . 7 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))))
112	111	eqreu 3691	. . . . . 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 12465	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
116	115	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
117	1	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118	116, 117	subeq0bd 11564	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119	118	fveq2d 6830	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
120	46	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121	119, 120	eqtrd 2764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
122	78	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123	122, 80	sylnib 328	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124	123	iffalsed 4489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126	121, 124, 125	3eqtr4rd 2775	. . . . . 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 2766	. . . . . . . . . . . 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 2814	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137	136	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138	137	iftrued 4486	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
139	4	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140	139	ffvelcdmda 7022	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘𝑥) ∈ (0..^𝑁))
141	138, 140	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142	134, 141	eqeltrrd 2829	. . . . . . . . . 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 3121	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148		eleq1 2816	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149		fveq2 6826	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑇‘𝑥) = (𝑇‘𝑁))
150		fvoveq1 7376	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151	148, 149, 150	ifbieq12d 4507	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152	151	eqeq2d 2740	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153	152	eqreu 3691	. . . . . 6 ⊢ ((𝑁 ∈ 𝐽 ∧ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154	114, 126, 147, 153	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
155	23	eleq2d 2814	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (0..^(𝑁 + 1))))
156	155	biimpa 476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157		fzosplitsni 13699	. . . . . . 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 3121	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162		s1len 14531	. . . . . . . 8 ⊢ (♯‘⟨“𝑁”⟩) = 1
163	15, 162	oveq12i 7365	. . . . . . 7 ⊢ ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164	163	oveq2i 7364	. . . . . 6 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165	164, 11	eqtr4i 2755	. . . . 5 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166	165	mpteq1i 5186	. . . 4 ⊢ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥 ∈ 𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167	166	f1ompt 7049	. . 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 7386	. . . . 5 ⊢ (0..^𝑁) ∈ V
170		fex 7166	. . . . 5 ⊢ ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
171	4, 169, 170	sylancl 586	. . . 4 ⊢ (𝜑 → 𝑇 ∈ V)
172		s1cli 14530	. . . 4 ⊢ ⟨“𝑁”⟩ ∈ Word V
173		ccatfval 14498	. . . 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 1540 ∈ wcel 2109 ∀wral 3044 ∃!wreu 3343 Vcvv 3438 ⊆ wss 3905 ifcif 4478 ↦ cmpt 5176 ^◡ccnv 5622 ⟶wf 6482 –1-1-onto→wf1o 6485 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 0cc0 11028 1c1 11029 + caddc 11031 − cmin 11365 ℕ₀cn0 12402 ℤ_≥cuz 12753 ..^cfzo 13575 ♯chash 14255 Word cword 14438 ++ cconcat 14495 ⟨“cs1 14520

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 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 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-nn 12147 df-n0 12403 df-z 12490 df-uz 12754 df-fz 13429 df-fzo 13576 df-hash 14256 df-word 14439 df-concat 14496 df-s1 14521

This theorem is referenced by: 1arithidomlem2 33486

W3C validator