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 32920
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 14552 . . . . . . . . . . . 12 (𝑇:(0..^𝑁)⟶(0..^𝑁) → 𝑇 ∈ Word (0..^𝑁))
6 lencl 14567 . . . . . . . . . . . 12 (𝑇 ∈ Word (0..^𝑁) → (♯‘𝑇) ∈ ℕ0)
74, 5, 63syl 18 . . . . . . . . . . 11 (𝜑 → (♯‘𝑇) ∈ ℕ0)
81, 7eqeltrid 2842 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
9 fzossfzop1 13778 . . . . . . . . . 10 (𝑁 ∈ ℕ0 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
108, 9syl 17 . . . . . . . . 9 (𝜑 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
11 ccatws1f1o.2 . . . . . . . . 9 𝐽 = (0..^(𝑁 + 1))
1210, 11sseqtrrdi 4046 . . . . . . . 8 (𝜑 → (0..^𝑁) ⊆ 𝐽)
1312adantr 480 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → (0..^𝑁) ⊆ 𝐽)
144adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
151eqcomi 2743 . . . . . . . . . . . 12 (♯‘𝑇) = 𝑁
1615a1i 11 . . . . . . . . . . 11 (𝜑 → (♯‘𝑇) = 𝑁)
1716oveq2d 7446 . . . . . . . . . 10 (𝜑 → (0..^(♯‘𝑇)) = (0..^𝑁))
1817eleq2d 2824 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0..^𝑁)))
1918biimpa 476 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^𝑁))
2014, 19ffvelcdmd 7104 . . . . . . 7 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇𝑥) ∈ (0..^𝑁))
2113, 20sseldd 3995 . . . . . 6 ((𝜑𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇𝑥) ∈ 𝐽)
2221adantlr 715 . . . . 5 (((𝜑𝑥𝐽) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇𝑥) ∈ 𝐽)
2311a1i 11 . . . . . . . . . . . . 13 (𝜑𝐽 = (0..^(𝑁 + 1)))
24 fzo0ssnn0 13781 . . . . . . . . . . . . 13 (0..^(𝑁 + 1)) ⊆ ℕ0
2523, 24eqsstrdi 4049 . . . . . . . . . . . 12 (𝜑𝐽 ⊆ ℕ0)
2625sselda 3994 . . . . . . . . . . 11 ((𝜑𝑥𝐽) → 𝑥 ∈ ℕ0)
2726nn0cnd 12586 . . . . . . . . . 10 ((𝜑𝑥𝐽) → 𝑥 ∈ ℂ)
2827adantr 480 . . . . . . . . 9 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
29 nn0uz 12917 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
308, 29eleqtrdi 2848 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘0))
3130ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁 ∈ (ℤ‘0))
3223eleq2d 2824 . . . . . . . . . . . . . 14 (𝜑 → (𝑥𝐽𝑥 ∈ (0..^(𝑁 + 1))))
3332biimpa 476 . . . . . . . . . . . . 13 ((𝜑𝑥𝐽) → 𝑥 ∈ (0..^(𝑁 + 1)))
3433adantr 480 . . . . . . . . . . . 12 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(𝑁 + 1)))
35 fzosplitsni 13813 . . . . . . . . . . . . 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 878 . . . . . . . . . 10 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = 𝑁)
4241, 1eqtrdi 2790 . . . . . . . . 9 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 = (♯‘𝑇))
4328, 42subeq0bd 11686 . . . . . . . 8 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 − (♯‘𝑇)) = 0)
4443fveq2d 6910 . . . . . . 7 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
45 s1fv 14644 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (⟨“𝑁”⟩‘0) = 𝑁)
468, 45syl 17 . . . . . . . 8 (𝜑 → (⟨“𝑁”⟩‘0) = 𝑁)
4746ad2antrr 726 . . . . . . 7 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘0) = 𝑁)
4844, 47eqtrd 2774 . . . . . 6 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
49 fzonn0p1 13777 . . . . . . . . 9 (𝑁 ∈ ℕ0𝑁 ∈ (0..^(𝑁 + 1)))
508, 49syl 17 . . . . . . . 8 (𝜑𝑁 ∈ (0..^(𝑁 + 1)))
5150, 11eleqtrrdi 2849 . . . . . . 7 (𝜑𝑁𝐽)
5251ad2antrr 726 . . . . . 6 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑁𝐽)
5348, 52eqeltrd 2838 . . . . 5 (((𝜑𝑥𝐽) ∧ ¬ 𝑥 ∈ (0..^(♯‘𝑇))) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) ∈ 𝐽)
5422, 53ifclda 4565 . . . 4 ((𝜑𝑥𝐽) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽)
5554ralrimiva 3143 . . 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 7103 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇𝑦) ∈ (0..^𝑁))
6256, 61sseldd 3995 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇𝑦) ∈ 𝐽)
631oveq2i 7441 . . . . . . . . 9 (0..^𝑁) = (0..^(♯‘𝑇))
6461, 63eleqtrdi 2848 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇𝑦) ∈ (0..^(♯‘𝑇)))
6564iftrued 4538 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))) = (𝑇‘(𝑇𝑦)))
662ad2antrr 726 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
67 simpr 484 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ (0..^𝑁))
68 f1ocnvfv2 7296 . . . . . . . 8 ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(𝑇𝑦)) = 𝑦)
6966, 67, 68syl2anc 584 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → (𝑇‘(𝑇𝑦)) = 𝑦)
7065, 69eqtr2d 2775 . . . . . 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 13709 . . . . . . . . . . . . . . . . . . . . 21 ¬ 𝑁 ∈ (0..^𝑁)
7978a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
8063eleq2i 2830 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (0..^𝑁) ↔ 𝑁 ∈ (0..^(♯‘𝑇)))
8179, 80sylnib 328 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
8277, 81eqneltrd 2858 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑥 ∈ (0..^(♯‘𝑇)))
8382iffalsed 4541 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))
8411, 24eqsstri 4029 . . . . . . . . . . . . . . . . . . . . . 22 𝐽 ⊆ ℕ0
85 simpllr 776 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥𝐽)
8684, 85sselid 3992 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℕ0)
8786nn0cnd 12586 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 ∈ ℂ)
8877, 1eqtrdi 2790 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑥 = (♯‘𝑇))
8987, 88subeq0bd 11686 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (𝑥 − (♯‘𝑇)) = 0)
9089fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
9146ad5antr 734 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
9290, 91eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = 𝑁)
9376, 83, 923eqtrd 2778 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → 𝑦 = 𝑁)
9493, 79eqneltrd 2858 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 = 𝑁) → ¬ 𝑦 ∈ (0..^𝑁))
9575, 94pm2.65da 817 . . . . . . . . . . . . . 14 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 = 𝑁)
9674, 95olcnd 877 . . . . . . . . . . . . 13 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^𝑁))
9796, 63eleqtrdi 2848 . . . . . . . . . . . 12 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 ∈ (0..^(♯‘𝑇)))
9897iftrued 4538 . . . . . . . . . . 11 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇𝑥))
9971, 98eqtrd 2774 . . . . . . . . . 10 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑦 = (𝑇𝑥))
10099fveq2d 6910 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑇𝑦) = (𝑇‘(𝑇𝑥)))
10166ad2antrr 726 . . . . . . . . . 10 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))
102 f1ocnvfv1 7295 . . . . . . . . . 10 ((𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇‘(𝑇𝑥)) = 𝑥)
103101, 96, 102syl2anc 584 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑇‘(𝑇𝑥)) = 𝑥)
104100, 103eqtr2d 2775 . . . . . . . 8 (((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = (𝑇𝑦))
105104ex 412 . . . . . . 7 ((((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) ∧ 𝑥𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (𝑇𝑦)))
106105ralrimiva 3143 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (𝑇𝑦)))
107 eleq1 2826 . . . . . . . . 9 (𝑥 = (𝑇𝑦) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ (𝑇𝑦) ∈ (0..^(♯‘𝑇))))
108 fveq2 6906 . . . . . . . . 9 (𝑥 = (𝑇𝑦) → (𝑇𝑥) = (𝑇‘(𝑇𝑦)))
109 fvoveq1 7453 . . . . . . . . 9 (𝑥 = (𝑇𝑦) → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇))))
110107, 108, 109ifbieq12d 4558 . . . . . . . 8 (𝑥 = (𝑇𝑦) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))))
111110eqeq2d 2745 . . . . . . 7 (𝑥 = (𝑇𝑦) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇))))))
112111eqreu 3737 . . . . . 6 (((𝑇𝑦) ∈ 𝐽𝑦 = if((𝑇𝑦) ∈ (0..^(♯‘𝑇)), (𝑇‘(𝑇𝑦)), (⟨“𝑁”⟩‘((𝑇𝑦) − (♯‘𝑇)))) ∧ ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = (𝑇𝑦))) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
11362, 70, 106, 112syl3anc 1370 . . . . 5 (((𝜑𝑦𝐽) ∧ 𝑦 ∈ (0..^𝑁)) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
11451ad2antrr 726 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑁𝐽)
1158nn0cnd 12586 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
116115ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑁 ∈ ℂ)
1171a1i 11 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑁 = (♯‘𝑇))
118116, 117subeq0bd 11686 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (𝑁 − (♯‘𝑇)) = 0)
119118fveq2d 6910 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = (⟨“𝑁”⟩‘0))
12046ad2antrr 726 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘0) = 𝑁)
121119, 120eqtrd 2774 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))) = 𝑁)
12278a1i 11 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^𝑁))
123122, 80sylnib 328 . . . . . . . 8 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ¬ 𝑁 ∈ (0..^(♯‘𝑇)))
124123iffalsed 4541 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
125 simpr 484 . . . . . . 7 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → 𝑦 = 𝑁)
126121, 124, 1253eqtr4rd 2785 . . . . . 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 2776 . . . . . . . . . . . 12 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
134133adantr 480 . . . . . . . . . . 11 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = 𝑁)
13563a1i 11 . . . . . . . . . . . . . . 15 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (0..^𝑁) = (0..^(♯‘𝑇)))
136135eleq2d 2824 . . . . . . . . . . . . . 14 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → (𝑥 ∈ (0..^𝑁) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
137136biimpa 476 . . . . . . . . . . . . 13 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝑇)))
138137iftrued 4538 . . . . . . . . . . . 12 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = (𝑇𝑥))
1394ad4antr 732 . . . . . . . . . . . . 13 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑇:(0..^𝑁)⟶(0..^𝑁))
140139ffvelcdmda 7103 . . . . . . . . . . . 12 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → (𝑇𝑥) ∈ (0..^𝑁))
141138, 140eqeltrd 2838 . . . . . . . . . . 11 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ (0..^𝑁))
142134, 141eqeltrrd 2839 . . . . . . . . . 10 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑁 ∈ (0..^𝑁))
14378a1i 11 . . . . . . . . . 10 ((((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) ∧ 𝑥 ∈ (0..^𝑁)) → ¬ 𝑁 ∈ (0..^𝑁))
144142, 143pm2.65da 817 . . . . . . . . 9 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → ¬ 𝑥 ∈ (0..^𝑁))
145130, 144orcnd 878 . . . . . . . 8 (((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) ∧ 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) → 𝑥 = 𝑁)
146145ex 412 . . . . . . 7 ((((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) ∧ 𝑥𝐽) → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
147146ralrimiva 3143 . . . . . 6 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁))
148 eleq1 2826 . . . . . . . . 9 (𝑥 = 𝑁 → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(♯‘𝑇))))
149 fveq2 6906 . . . . . . . . 9 (𝑥 = 𝑁 → (𝑇𝑥) = (𝑇𝑁))
150 fvoveq1 7453 . . . . . . . . 9 (𝑥 = 𝑁 → (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))) = (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))
151148, 149, 150ifbieq12d 4558 . . . . . . . 8 (𝑥 = 𝑁 → if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))))
152151eqeq2d 2745 . . . . . . 7 (𝑥 = 𝑁 → (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ↔ 𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇))))))
153152eqreu 3737 . . . . . 6 ((𝑁𝐽𝑦 = if(𝑁 ∈ (0..^(♯‘𝑇)), (𝑇𝑁), (⟨“𝑁”⟩‘(𝑁 − (♯‘𝑇)))) ∧ ∀𝑥𝐽 (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) → 𝑥 = 𝑁)) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
154114, 126, 147, 153syl3anc 1370 . . . . 5 (((𝜑𝑦𝐽) ∧ 𝑦 = 𝑁) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
15523eleq2d 2824 . . . . . . 7 (𝜑 → (𝑦𝐽𝑦 ∈ (0..^(𝑁 + 1))))
156155biimpa 476 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ (0..^(𝑁 + 1)))
157 fzosplitsni 13813 . . . . . . 7 (𝑁 ∈ (ℤ‘0) → (𝑦 ∈ (0..^(𝑁 + 1)) ↔ (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁)))
158157biimpa 476 . . . . . 6 ((𝑁 ∈ (ℤ‘0) ∧ 𝑦 ∈ (0..^(𝑁 + 1))) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
159127, 156, 158syl2anc 584 . . . . 5 ((𝜑𝑦𝐽) → (𝑦 ∈ (0..^𝑁) ∨ 𝑦 = 𝑁))
160113, 154, 159mpjaodan 960 . . . 4 ((𝜑𝑦𝐽) → ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
161160ralrimiva 3143 . . 3 (𝜑 → ∀𝑦𝐽 ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
162 s1len 14640 . . . . . . . 8 (♯‘⟨“𝑁”⟩) = 1
16315, 162oveq12i 7442 . . . . . . 7 ((♯‘𝑇) + (♯‘⟨“𝑁”⟩)) = (𝑁 + 1)
164163oveq2i 7441 . . . . . 6 (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = (0..^(𝑁 + 1))
165164, 11eqtr4i 2765 . . . . 5 (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) = 𝐽
166165mpteq1i 5243 . . . 4 (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))) = (𝑥𝐽 ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))))
167166f1ompt 7130 . . 3 ((𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽1-1-onto𝐽 ↔ (∀𝑥𝐽 if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇)))) ∈ 𝐽 ∧ ∀𝑦𝐽 ∃!𝑥𝐽 𝑦 = if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))))
16855, 161, 167sylanbrc 583 . 2 (𝜑 → (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘⟨“𝑁”⟩))) ↦ if(𝑥 ∈ (0..^(♯‘𝑇)), (𝑇𝑥), (⟨“𝑁”⟩‘(𝑥 − (♯‘𝑇))))):𝐽1-1-onto𝐽)
169 ovex 7463 . . . . 5 (0..^𝑁) ∈ V
170 fex 7245 . . . . 5 ((𝑇:(0..^𝑁)⟶(0..^𝑁) ∧ (0..^𝑁) ∈ V) → 𝑇 ∈ V)
1714, 169, 170sylancl 586 . . . 4 (𝜑𝑇 ∈ V)
172 s1cli 14639 . . . 4 ⟨“𝑁”⟩ ∈ Word V
173 ccatfval 14607 . . . 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 847   = wceq 1536  wcel 2105  wral 3058  ∃!wreu 3375  Vcvv 3477  wss 3962  ifcif 4530  cmpt 5230  ccnv 5687  wf 6558  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  cc 11150  0cc0 11152  1c1 11153   + caddc 11155  cmin 11489  0cn0 12523  cuz 12875  ..^cfzo 13690  chash 14365  Word cword 14548   ++ cconcat 14604  ⟨“cs1 14629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-hash 14366  df-word 14549  df-concat 14605  df-s1 14630
This theorem is referenced by:  1arithidomlem2  33543
  Copyright terms: Public domain W3C validator