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

Theorem ccatws1f1o 32936
Description: Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025.)
Hypotheses
Ref Expression
ccatws1f1o.1 𝑁 = (♯‘𝑇)
ccatws1f1o.2 𝐽 = (0..^(𝑁 + 1))
ccatws1f1o.3 (𝜑𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
Assertion
Ref Expression
ccatws1f1o (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽1-1-onto𝐽)

Proof of Theorem ccatws1f1o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ccatws1f1o.1 . . . . . . . . . . 11 𝑁 = (♯‘𝑇)
2 ccatws1f1o.3 . . . . . . . . . . . . 13 (𝜑𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
3 f1of 6848 . . . . . . . . . . . . 13 (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
42, 3syl 17 . . . . . . . . . . . 12 (𝜑𝑇:(0..^𝑁)⟶(0..^𝑁))
5 iswrdi 14556 . . . . . . . . . . . 12 (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6 lencl 14571 . . . . . . . . . . . 12 (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ0)
74, 5, 63syl 18 . . . . . . . . . . 11 (𝜑 → (♯‘𝑇) ∈ ℕ0)
81, 7eqeltrid 2845 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
9 fzossfzop1 13782 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
108, 9syl 17 . . . . . . . . 9 (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11 ccatws1f1o.2 . . . . . . . . 9 𝐽 = (0..^(𝑁 + 1))
1210, 11sseqtrrdi 4025 . . . . . . . 8 (𝜑 → (0..^𝑁) ⊆ 𝐽)
1312adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
144adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
151eqcomi 2746 . . . . . . . . . . . 12 (♯‘𝑇) = 𝑁
1615a1i 11 . . . . . . . . . . 11 (𝜑 → (♯‘𝑇) = 𝑁)
1716oveq2d 7447 . . . . . . . . . 10 (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
1817eleq2d 2827 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
1918biimpa 476 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
2014, 19ffvelcdmd 7105 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇𝑥) ∈ (0..^𝑁))
2113, 20sseldd 3984 . . . . . 6 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇𝑥) ∈ 𝐽)
2221adantlr 715 . . . . 5 (((𝜑𝑥𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇𝑥) ∈ 𝐽)
2311a1i 11 . . . . . . . . . . . . 13 (𝜑𝐽 = (0..^(𝑁 + 1)))
24 fzo0ssnn0 13785 . . . . . . . . . . . . 13 (0..^(𝑁 + 1)) ⊆ ℕ0
2523, 24eqsstrdi 4028 . . . . . . . . . . . 12 (𝜑𝐽 ⊆ ℕ0)
2625sselda 3983 . . . . . . . . . . 11 ((𝜑𝑥𝐽) → 𝑥 ∈ ℕ0)
2726nn0cnd 12589 . . . . . . . . . 10 ((𝜑𝑥𝐽) → 𝑥 ∈ ℂ)
2827adantr 480 . . . . . . . . 9 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29 nn0uz 12920 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
308, 29eleqtrdi 2851 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘0))
3130ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ‘0))
3223eleq2d 2827 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝐽𝑥 ∈ (0..^(𝑁 + 1))))
3332biimpa 476 . . . . . . . . . . . . 13 ((𝜑𝑥𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
3433adantr 480 . . . . . . . . . . . 12 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35 fzosplitsni 13817 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ‘0) → (𝑥 ∈ (0..^(𝑁 + 1)) ↔ (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁)))
3635biimpa 476 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘0) ∧ 𝑥 ∈ (0..^(𝑁 + 1))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
3731, 34, 36syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
3818notbid 318 . . . . . . . . . . . . 13 (𝜑 → (¬ 𝑥 ∈ (0..^(♯‘𝑇)) ↔ ¬ 𝑥 ∈ (0..^𝑁)))
3938biimpa 476 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → ¬ 𝑥 ∈ (0..^𝑁))
4039adantlr 715 . . . . . . . . . . 11 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → ¬ 𝑥 ∈ (0..^𝑁))
4137, 40orcnd 879 . . . . . . . . . 10 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = 𝑁)
4241, 1eqtrdi 2793 . . . . . . . . 9 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
4328, 42subeq0bd 11689 . . . . . . . 8 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
4443fveq2d 6910 . . . . . . 7 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45 s1fv 14648 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (⟨“𝑁”⟩‘0) = 𝑁)
468, 45syl 17 . . . . . . . 8 (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
4746ad2antrr 726 . . . . . . 7 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
4844, 47eqtrd 2777 . . . . . 6 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49 fzonn0p1 13781 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ (0..^(𝑁 + 1)))
508, 49syl 17 . . . . . . . 8 (𝜑𝑁 ∈ (0..^(𝑁 + 1)))
5150, 11eleqtrrdi 2852 . . . . . . 7 (𝜑𝑁𝐽)
5251ad2antrr 726 . . . . . 6 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁𝐽)
5348, 52eqeltrd 2841 . . . . 5 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
5422, 53ifclda 4561 . . . 4 ((𝜑𝑥𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
5554ralrimiva 3146 . . 3 (𝜑 → ∀𝑥𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
5612ad2antrr 726 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ 𝐽)
57 f1ocnv 6860 . . . . . . . . . 10 (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
58 f1of 6848 . . . . . . . . . 10 (𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
592, 57, 583syl 18 . . . . . . . . 9 (𝜑𝑇:(0..^𝑁)⟶(0..^𝑁))
6059adantr 480 . . . . . . . 8 ((𝜑𝑦𝐽) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
6160ffvelcdmda 7104 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇𝑦) ∈ (0..^𝑁))
6256, 61sseldd 3984 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇𝑦) ∈ 𝐽)
631oveq2i 7442 . . . . . . . . 9 (0..^𝑁) = (0..^(♯‘𝑇))
6461, 63eleqtrdi 2851 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇𝑦) ∈ (0..^(♯‘𝑇)))
6564iftrued 4533 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))) = (𝑇‘(𝑇𝑦)))
662ad2antrr 726 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67 simpr 484 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68 f1ocnvfv2 7297 . . . . . . . 8 ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(𝑇𝑦)) = 𝑦)
6966, 67, 68syl2anc 584 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(𝑇𝑦)) = 𝑦)
7065, 69eqtr2d 2778 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))))
71 simpr 484 . . . . . . . . . . 11 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
7230adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐽) → 𝑁 ∈ (ℤ‘0))
7372, 33, 36syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐽) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
7473ad5ant14 758 . . . . . . . . . . . . . 14 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
7567ad3antrrr 730 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 ∈ (0..^𝑁))
7671adantr 480 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
77 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = 𝑁)
78 fzonel 13713 . . . . . . . . . . . . . . . . . . . . 21 ¬ 𝑁 ∈ (0..^𝑁)
7978a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
8063eleq2i 2833 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
8179, 80sylnib 328 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
8277, 81eqneltrd 2861 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
8382iffalsed 4536 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
8411, 24eqsstri 4030 . . . . . . . . . . . . . . . . . . . . . 22 𝐽 ⊆ ℕ0
85 simpllr 776 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥𝐽)
8684, 85sselid 3981 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ0)
8786nn0cnd 12589 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
8877, 1eqtrdi 2793 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
8987, 88subeq0bd 11689 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
9089fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
9146ad5antr 734 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
9290, 91eqtrd 2777 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
9376, 83, 923eqtrd 2781 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
9493, 79eqneltrd 2861 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑦 ∈ (0..^𝑁))
9575, 94pm2.65da 817 . . . . . . . . . . . . . 14 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 = 𝑁)
9674, 95olcnd 878 . . . . . . . . . . . . 13 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^𝑁))
9796, 63eleqtrdi 2851 . . . . . . . . . . . 12 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
9897iftrued 4533 . . . . . . . . . . 11 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇𝑥))
9971, 98eqtrd 2777 . . . . . . . . . 10 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇𝑥))
10099fveq2d 6910 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑇𝑦) = (𝑇‘(𝑇𝑥)))
10166ad2antrr 726 . . . . . . . . . 10 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102 f1ocnvfv1 7296 . . . . . . . . . 10 ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘(𝑇𝑥)) = 𝑥)
103101, 96, 102syl2anc 584 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑇‘(𝑇𝑥)) = 𝑥)
104100, 103eqtr2d 2778 . . . . . . . 8 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (𝑇𝑦))
105104ex 412 . . . . . . 7 ((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (𝑇𝑦)))
106105ralrimiva 3146 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (𝑇𝑦)))
107 eleq1 2829 . . . . . . . . 9 (𝑥 = (𝑇𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (𝑇𝑦) ∈ (0..^(♯‘𝑇))))
108 fveq2 6906 . . . . . . . . 9 (𝑥 = (𝑇𝑦) → (𝑇𝑥) = (𝑇‘(𝑇𝑦)))
109 fvoveq1 7454 . . . . . . . . 9 (𝑥 = (𝑇𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇))))
110107, 108, 109ifbieq12d 4554 . . . . . . . 8 (𝑥 = (𝑇𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))))
111110eqeq2d 2748 . . . . . . 7 (𝑥 = (𝑇𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇))))))
112111eqreu 3735 . . . . . 6 (((𝑇𝑦) ∈ 𝐽𝑦 = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))) ∧ ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (𝑇𝑦))) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
11362, 70, 106, 112syl3anc 1373 . . . . 5 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
11451ad2antrr 726 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑁𝐽)
1158nn0cnd 12589 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
116115ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
1171a1i 11 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118116, 117subeq0bd 11689 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119118fveq2d 6910 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
12046ad2antrr 726 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121119, 120eqtrd 2777 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
12278a1i 11 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123122, 80sylnib 328 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124123iffalsed 4536 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125 simpr 484 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126121, 124, 1253eqtr4rd 2788 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
12730adantr 480 . . . . . . . . . . 11 ((𝜑𝑦𝐽) → 𝑁 ∈ (ℤ‘0))
128127ad3antrrr 730 . . . . . . . . . 10 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑁 ∈ (ℤ‘0))
12933ad5ant14 758 . . . . . . . . . 10 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(𝑁 + 1)))
130128, 129, 36syl2anc 584 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ∨ 𝑥 = 𝑁))
131 simpr 484 . . . . . . . . . . . . 13 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
132 simpllr 776 . . . . . . . . . . . . 13 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = 𝑁)
133131, 132eqtr3d 2779 . . . . . . . . . . . 12 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
134133adantr 480 . . . . . . . . . . 11 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
13563a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (0..^𝑁) = (0..^(♯‘𝑇)))
136135eleq2d 2827 . . . . . . . . . . . . . 14 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137136biimpa 476 . . . . . . . . . . . . 13 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138137iftrued 4533 . . . . . . . . . . . 12 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇𝑥))
1394ad4antr 732 . . . . . . . . . . . . 13 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140139ffvelcdmda 7104 . . . . . . . . . . . 12 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇𝑥) ∈ (0..^𝑁))
141138, 140eqeltrd 2841 . . . . . . . . . . 11 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142134, 141eqeltrrd 2842 . . . . . . . . . 10 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑁 ∈ (0..^𝑁))
14378a1i 11 . . . . . . . . . 10 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → ¬ 𝑁 ∈ (0..^𝑁))
144142, 143pm2.65da 817 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 ∈ (0..^𝑁))
145130, 144orcnd 879 . . . . . . . 8 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = 𝑁)
146145ex 412 . . . . . . 7 ((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
147146ralrimiva 3146 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148 eleq1 2829 . . . . . . . . 9 (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149 fveq2 6906 . . . . . . . . 9 (𝑥 = 𝑁 → (𝑇𝑥) = (𝑇𝑁))
150 fvoveq1 7454 . . . . . . . . 9 (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151148, 149, 150ifbieq12d 4554 . . . . . . . 8 (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152151eqeq2d 2748 . . . . . . 7 (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153152eqreu 3735 . . . . . 6 ((𝑁𝐽𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154114, 126, 147, 153syl3anc 1373 . . . . 5 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
15523eleq2d 2827 . . . . . . 7 (𝜑 → (𝑦𝐽𝑦 ∈ (0..^(𝑁 + 1))))
156155biimpa 476 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157 fzosplitsni 13817 . . . . . . 7 (𝑁 ∈ (ℤ‘0) → (𝑦 ∈ (0..^(𝑁 + 1)) ↔ (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁)))
158157biimpa 476 . . . . . 6 ((𝑁 ∈ (ℤ‘0) ∧ 𝑦 ∈ (0..^(𝑁 + 1))) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
159127, 156, 158syl2anc 584 . . . . 5 ((𝜑𝑦𝐽) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
160113, 154, 159mpjaodan 961 . . . 4 ((𝜑𝑦𝐽) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
161160ralrimiva 3146 . . 3 (𝜑 → ∀𝑦𝐽 ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162 s1len 14644 . . . . . . . 8 (♯‘⟨“𝑁”⟩) = 1
16315, 162oveq12i 7443 . . . . . . 7 ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164163oveq2i 7442 . . . . . 6 (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165164, 11eqtr4i 2768 . . . . 5 (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166165mpteq1i 5238 . . . 4 (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167166f1ompt 7131 . . 3 ((𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽1-1-onto𝐽 ↔ (∀𝑥𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽 ∧ ∀𝑦𝐽 ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
16855, 161, 167sylanbrc 583 . 2 (𝜑 → (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽1-1-onto𝐽)
169 ovex 7464 . . . . 5 (0..^𝑁) ∈ V
170 fex 7246 . . . . 5 ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
1714, 169, 170sylancl 586 . . . 4 (𝜑𝑇 ∈ V)
172 s1cli 14643 . . . 4 ⟨“𝑁”⟩ ∈ Word V
173 ccatfval 14611 . . . 4 ((𝑇 ∈ V ∧ ⟨“𝑁”⟩ ∈ Word V) → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
174171, 172, 173sylancl 586 . . 3 (𝜑 → (𝑇 ++ ⟨“𝑁”⟩) = (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
175174f1oeq1d 6843 . 2 (𝜑 → ((𝑇 ++ ⟨“𝑁”⟩):𝐽1-1-onto𝐽 ↔ (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽1-1-onto𝐽))
176168, 175mpbird 257 1 (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽1-1-onto𝐽)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848   = wceq 1540  wcel 2108  wral 3061  ∃!wreu 3378  Vcvv 3480  wss 3951  ifcif 4525  cmpt 5225  ccnv 5684  wf 6557  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cc 11153  0cc0 11155  1c1 11156   + caddc 11158  cmin 11492  0cn0 12526  cuz 12878  ..^cfzo 13694  chash 14369  Word cword 14552   ++ cconcat 14608  ⟨“cs1 14633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-hash 14370  df-word 14553  df-concat 14609  df-s1 14634
This theorem is referenced by:  1arithidomlem2  33564
  Copyright terms: Public domain W3C validator