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 33496

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 6816	. . . . . . . . . . . . 13 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
4	2, 3	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇:(0..^𝑁)⟶(0..^𝑁))
5		iswrdi 14642	. . . . . . . . . . . 12 ⊢ (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6		lencl 14658	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ₀)
7	4, 5, 6	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) ∈ ℕ₀)
8	1, 7	eqeltrid 2865	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
9		fzossfzop1 13858	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
10	8, 9	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11		ccatws1f1o.2	. . . . . . . . 9 ⊢ 𝐽 = (0..^(𝑁 + 1))
12	10, 11	sseqtrrdi 3972	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑁) ⊆ 𝐽)
13	12	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
14	4	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
15	1	eqcomi 2770	. . . . . . . . . . . 12 ⊢ (♯‘𝑇) = 𝑁
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑇) = 𝑁)
17	16	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
18	17	eleq2d 2847	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
19	18	biimpa 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
20	14, 19	ffvelcdmd 7077	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ (0..^𝑁))
21	13, 20	sseldd 3932	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
22	21	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ 𝐽)
23	11	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 = (0..^(𝑁 + 1)))
24		fzo0ssnn0 13861	. . . . . . . . . . . . 13 ⊢ (0..^(𝑁 + 1)) ⊆ ℕ₀
25	23, 24	eqsstrdi 3975	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ ℕ₀)
26	25	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ₀)
27	26	nn0cnd 12650	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℂ)
28	27	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29		nn0uz 12984	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
30	8, 29	eleqtrdi 2871	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
31	30	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ_≥‘0))
32	23	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ (0..^(𝑁 + 1))))
33	32	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
34	33	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35		fzosplitsni 13894	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (𝑥 ∈ (0..^(𝑁 + 1)) ↔ (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁)))
36	35	biimpa 482	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘0) ∧ 𝑥 ∈ (0..^(𝑁 + 1))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
37	31, 34, 36	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
38	18	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ 𝑥 ∈ (0..^(♯‘𝑇)) ↔ ¬ 𝑥 ∈ (0..^𝑁)))
39	38	biimpa 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → ¬ 𝑥 ∈ (0..^𝑁))
40	39	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → ¬ 𝑥 ∈ (0..^𝑁))
41	37, 40	orcnd 892	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = 𝑁)
42	41, 1	eqtrdi 2812	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
43	28, 42	subeq0bd 11723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
44	43	fveq2d 6881	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45		s1fv 14738	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (⟨“𝑁”⟩‘0) = 𝑁)
46	8, 45	syl 18	. . . . . . . 8 ⊢ (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
47	46	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
48	44, 47	eqtrd 2796	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49		fzonn0p1 13857	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0..^(𝑁 + 1)))
50	8, 49	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(𝑁 + 1)))
51	50, 11	eleqtrrdi 2872	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ 𝐽)
52	51	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ 𝐽)
53	48, 52	eqeltrd 2861	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
54	22, 53	ifclda 4518	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
55	54	ralrimiva 3155	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
56	12	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ 𝐽)
57		f1ocnv 6829	. . . . . . . . . 10 ⊢ (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → ^◡𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
58		f1of 6816	. . . . . . . . . 10 ⊢ (^◡𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → ^◡𝑇:(0..^𝑁)⟶(0..^𝑁))
59	2, 57, 58	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝑇:(0..^𝑁)⟶(0..^𝑁))
60	59	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ^◡𝑇:(0..^𝑁)⟶(0..^𝑁))
61	60	ffvelcdmda 7076	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^𝑁))
62	56, 61	sseldd 3932	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ 𝐽)
63	1	oveq2i 7423	. . . . . . . . 9 ⊢ (0..^𝑁) = (0..^(♯‘𝑇))
64	61, 63	eleqtrdi 2871	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)))
65	64	iftrued 4490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) = (𝑇‘(^◡𝑇‘𝑦)))
66	2	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68		f1ocnvfv2 7277	. . . . . . . 8 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
69	66, 67, 68	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(^◡𝑇‘𝑦)) = 𝑦)
70	65, 69	eqtr2d 2797	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
71		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
72	30	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑁 ∈ (ℤ_≥‘0))
73	72, 33, 36	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
74	73	ad5ant14 770	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
75	67	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 ∈ (0..^𝑁))
76	71	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
77		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = 𝑁)
78		fzonel 13788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 𝑁 ∈ (0..^𝑁)
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
80	63	eleq2i 2853	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
81	79, 80	sylnib 331	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
82	77, 81	eqneltrd 2881	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
83	82	iffalsed 4493	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
84	11, 24	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 ⊆ ℕ₀
85		simpllr 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ 𝐽)
86	84, 85	sselid 3929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ₀)
87	86	nn0cnd 12650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
88	77, 1	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
89	87, 88	subeq0bd 11723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
90	89	fveq2d 6881	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
91	46	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
92	90, 91	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
93	76, 83, 92	3eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
94	93, 79	eqneltrd 2881	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑦 ∈ (0..^𝑁))
95	75, 94	pm2.65da 829	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 = 𝑁)
96	74, 95	olcnd 891	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^𝑁))
97	96, 63	eleqtrdi 2871	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
98	97	iftrued 4490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
99	71, 98	eqtrd 2796	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇‘𝑥))
100	99	fveq2d 6881	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘𝑦) = (^◡𝑇‘(𝑇‘𝑥)))
101	66	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102		f1ocnvfv1 7276	. . . . . . . . . 10 ⊢ ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
103	101, 96, 102	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (^◡𝑇‘(𝑇‘𝑥)) = 𝑥)
104	100, 103	eqtr2d 2797	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (^◡𝑇‘𝑦))
105	104	ex 418	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
106	105	ralrimiva 3155	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦)))
107		eleq1 2849	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇))))
108		fveq2 6877	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑇‘𝑥) = (𝑇‘(^◡𝑇‘𝑦)))
109		fvoveq1 7435	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))
110	107, 108, 109	ifbieq12d 4511	. . . . . . . 8 ⊢ (𝑥 = (^◡𝑇‘𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))))
111	110	eqeq2d 2772	. . . . . . 7 ⊢ (𝑥 = (^◡𝑇‘𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇))))))
112	111	eqreu 3687	. . . . . 6 ⊢ (((^◡𝑇‘𝑦) ∈ 𝐽 ∧ 𝑦 = if((^◡𝑇‘𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(^◡𝑇‘𝑦)), (⟨“𝑁”⟩‘((^◡𝑇‘𝑦) − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (^◡𝑇‘𝑦))) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
113	62, 70, 106, 112	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
114	51	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ 𝐽)
115	8	nn0cnd 12650	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
116	115	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
117	1	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118	116, 117	subeq0bd 11723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119	118	fveq2d 6881	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
120	46	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121	119, 120	eqtrd 2796	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
122	78	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123	122, 80	sylnib 331	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124	123	iffalsed 4493	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126	121, 124, 125	3eqtr4rd 2807	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
127	30	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑁 ∈ (ℤ_≥‘0))
128	127	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑁 ∈ (ℤ_≥‘0))
129	33	ad5ant14 770	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(𝑁 + 1)))
130	128, 129, 36	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
131		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
132		simpllr 788	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = 𝑁)
133	131, 132	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
134	133	adantr 486	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
135	63	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (0..^𝑁) = (0..^(♯‘𝑇)))
136	135	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137	136	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138	137	iftrued 4490	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇‘𝑥))
139	4	ad4antr 745	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140	139	ffvelcdmda 7076	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘𝑥) ∈ (0..^𝑁))
141	138, 140	eqeltrd 2861	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142	134, 141	eqeltrrd 2862	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑁 ∈ (0..^𝑁))
143	78	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → ¬ 𝑁 ∈ (0..^𝑁))
144	142, 143	pm2.65da 829	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 ∈ (0..^𝑁))
145	130, 144	orcnd 892	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = 𝑁)
146	145	ex 418	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥 ∈ 𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
147	146	ralrimiva 3155	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148		eleq1 2849	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149		fveq2 6877	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (𝑇‘𝑥) = (𝑇‘𝑁))
150		fvoveq1 7435	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151	148, 149, 150	ifbieq12d 4511	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152	151	eqeq2d 2772	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153	152	eqreu 3687	. . . . . 6 ⊢ ((𝑁 ∈ 𝐽 ∧ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥 ∈ 𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154	114, 126, 147, 153	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
155	23	eleq2d 2847	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (0..^(𝑁 + 1))))
156	155	biimpa 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157		fzosplitsni 13894	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (𝑦 ∈ (0..^(𝑁 + 1)) ↔ (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁)))
158	157	biimpa 482	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘0) ∧ 𝑦 ∈ (0..^(𝑁 + 1))) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
159	127, 156, 158	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
160	113, 154, 159	mpjaodan 973	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
161	160	ralrimiva 3155	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162		s1len 14733	. . . . . . . 8 ⊢ (♯‘⟨“𝑁”⟩) = 1
163	15, 162	oveq12i 7424	. . . . . . 7 ⊢ ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164	163	oveq2i 7423	. . . . . 6 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165	164, 11	eqtr4i 2787	. . . . 5 ⊢ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166	165	mpteq1i 5196	. . . 4 ⊢ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥 ∈ 𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167	166	f1ompt 7103	. . 3 ⊢ ((𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽–1-1-onto→𝐽 ↔ (∀𝑥 ∈ 𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽 ∧ ∀𝑦 ∈ 𝐽 ∃!𝑥 ∈ 𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
168	55, 161, 167	sylanbrc 595	. 2 ⊢ (𝜑 → (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽–1-1-onto→𝐽)
169		ovex 7445	. . . . 5 ⊢ (0..^𝑁) ∈ V
170		fex 7224	. . . . 5 ⊢ ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
171	4, 169, 170	sylancl 598	. . . 4 ⊢ (𝜑 → 𝑇 ∈ V)
172		s1cli 14732	. . . 4 ⊢ ⟨“𝑁”⟩ ∈ Word V
173		ccatfval 14698	. . . 4 ⊢ ((𝑇 ∈ V ∧ ⟨“𝑁”⟩ ∈ Word V) → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
174	171, 172, 173	sylancl 598	. . 3 ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
175	174	f1oeq1d 6811	. 2 ⊢ (𝜑 → ((𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽 ↔ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇‘𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽–1-1-onto→𝐽))
176	168, 175	mpbird 260	1 ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ∃!wreu 3364 Vcvv 3451 ⊆ wss 3899 ifcif 4482 ↦ cmpt 5186 ^◡ccnv 5650 ⟶wf 6527 –1-1-onto→wf1o 6530 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 0cc0 11181 1c1 11182 + caddc 11184 − cmin 11522 ℕ₀cn0 12587 ℤ_≥cuz 12946 ..^cfzo 13768 ♯chash 14454 Word cword 14638 ++ cconcat 14695 ⟨“cs1 14722

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-n0 12588 df-z 12675 df-uz 12947 df-fz 13621 df-fzo 13769 df-hash 14455 df-word 14639 df-concat 14696 df-s1 14723

This theorem is used by: 1arithidomlem2 34050

W3C validator