ccatws1f1o

Description: Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	ccatws1f1o.1	$⊢ N = \|T\|$
	ccatws1f1o.2	$⊢ J = (0 ..^N + 1)$
	ccatws1f1o.3	$⊢ φ \to T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N)$
Assertion	ccatws1f1o	$⊢ φ \to (T ++ ⟨“ N ”⟩) : J \underset{1-1 onto}{⟶} J$

Proof

Step	Hyp	Ref	Expression
1		ccatws1f1o.1	$⊢ N = \|T\|$
2		ccatws1f1o.2	$⊢ J = (0 ..^N + 1)$
3		ccatws1f1o.3	$⊢ φ \to T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N)$
4		f1of	$⊢ T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N) \to T : (0 ..^N) ⟶ (0 ..^N)$
5	3 4	syl	$⊢ φ \to T : (0 ..^N) ⟶ (0 ..^N)$
6		iswrdi	$⊢ T : (0 ..^N) ⟶ (0 ..^N) \to T \in Word (0 ..^N)$
7		lencl	$⊢ T \in Word (0 ..^N) \to \|T\| \in ℕ_{0}$
8	5 6 7	3syl	$⊢ φ \to \|T\| \in ℕ_{0}$
9	1 8	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
10		fzossfzop1	$⊢ N \in ℕ_{0} \to (0 ..^N) \subseteq (0 ..^N + 1)$
11	9 10	syl	$⊢ φ \to (0 ..^N) \subseteq (0 ..^N + 1)$
12	11 2	sseqtrrdi	$⊢ φ \to (0 ..^N) \subseteq J$
13	12	adantr	$⊢ (φ \land x \in (0 ..^\|T\|)) \to (0 ..^N) \subseteq J$
14	5	adantr	$⊢ (φ \land x \in (0 ..^\|T\|)) \to T : (0 ..^N) ⟶ (0 ..^N)$
15	1	eqcomi	$⊢ \|T\| = N$
16	15	a1i	$⊢ φ \to \|T\| = N$
17	16	oveq2d	$⊢ φ \to (0 ..^\|T\|) = (0 ..^N)$
18	17	eleq2d	$⊢ φ \to (x \in (0 ..^\|T\|) \leftrightarrow x \in (0 ..^N))$
19	18	biimpa	$⊢ (φ \land x \in (0 ..^\|T\|)) \to x \in (0 ..^N)$
20	14 19	ffvelcdmd	$⊢ (φ \land x \in (0 ..^\|T\|)) \to T (x) \in (0 ..^N)$
21	13 20	sseldd	$⊢ (φ \land x \in (0 ..^\|T\|)) \to T (x) \in J$
22	21	adantlr	$⊢ ((φ \land x \in J) \land x \in (0 ..^\|T\|)) \to T (x) \in J$
23	2	a1i	$⊢ φ \to J = (0 ..^N + 1)$
24		fzo0ssnn0	$⊢ (0 ..^N + 1) \subseteq ℕ_{0}$
25	23 24	eqsstrdi	$⊢ φ \to J \subseteq ℕ_{0}$
26	25	sselda	$⊢ (φ \land x \in J) \to x \in ℕ_{0}$
27	26	nn0cnd	$⊢ (φ \land x \in J) \to x \in ℂ$
28	27	adantr	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to x \in ℂ$
29		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
30	9 29	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
31	30	ad2antrr	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to N \in ℤ_{\geq 0}$
32	23	eleq2d	$⊢ φ \to (x \in J \leftrightarrow x \in (0 ..^N + 1))$
33	32	biimpa	$⊢ (φ \land x \in J) \to x \in (0 ..^N + 1)$
34	33	adantr	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to x \in (0 ..^N + 1)$
35		fzosplitsni	$⊢ N \in ℤ_{\geq 0} \to (x \in (0 ..^N + 1) \leftrightarrow (x \in (0 ..^N) \lor x = N))$
36	35	biimpa	$⊢ (N \in ℤ_{\geq 0} \land x \in (0 ..^N + 1)) \to (x \in (0 ..^N) \lor x = N)$
37	31 34 36	syl2anc	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to (x \in (0 ..^N) \lor x = N)$
38	18	notbid	$⊢ φ \to (\neg x \in (0 ..^\|T\|) \leftrightarrow \neg x \in (0 ..^N))$
39	38	biimpa	$⊢ (φ \land \neg x \in (0 ..^\|T\|)) \to \neg x \in (0 ..^N)$
40	39	adantlr	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to \neg x \in (0 ..^N)$
41	37 40	orcnd	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to x = N$
42	41 1	eqtrdi	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to x = \|T\|$
43	28 42	subeq0bd	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to x - \|T\| = 0$
44	43	fveq2d	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to ⟨“ N ”⟩ (x - \|T\|) = ⟨“ N ”⟩ (0)$
45		s1fv	$⊢ N \in ℕ_{0} \to ⟨“ N ”⟩ (0) = N$
46	9 45	syl	$⊢ φ \to ⟨“ N ”⟩ (0) = N$
47	46	ad2antrr	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to ⟨“ N ”⟩ (0) = N$
48	44 47	eqtrd	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to ⟨“ N ”⟩ (x - \|T\|) = N$
49		fzonn0p1	$⊢ N \in ℕ_{0} \to N \in (0 ..^N + 1)$
50	9 49	syl	$⊢ φ \to N \in (0 ..^N + 1)$
51	50 2	eleqtrrdi	$⊢ φ \to N \in J$
52	51	ad2antrr	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to N \in J$
53	48 52	eqeltrd	$⊢ ((φ \land x \in J) \land \neg x \in (0 ..^\|T\|)) \to ⟨“ N ”⟩ (x - \|T\|) \in J$
54	22 53	ifclda	$⊢ (φ \land x \in J) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \in J$
55	54	ralrimiva	$⊢ φ \to \forall x \in J if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \in J$
56	12	ad2antrr	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to (0 ..^N) \subseteq J$
57		f1ocnv	$⊢ T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N) \to T^{-1} : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N)$
58		f1of	$⊢ T^{-1} : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N) \to T^{-1} : (0 ..^N) ⟶ (0 ..^N)$
59	3 57 58	3syl	$⊢ φ \to T^{-1} : (0 ..^N) ⟶ (0 ..^N)$
60	59	adantr	$⊢ (φ \land y \in J) \to T^{-1} : (0 ..^N) ⟶ (0 ..^N)$
61	60	ffvelcdmda	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to T^{-1} (y) \in (0 ..^N)$
62	56 61	sseldd	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to T^{-1} (y) \in J$
63	1	oveq2i	$⊢ (0 ..^N) = (0 ..^\|T\|)$
64	61 63	eleqtrdi	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to T^{-1} (y) \in (0 ..^\|T\|)$
65	64	iftrued	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to if (T^{-1} (y) \in (0 ..^\|T\|), T (T^{-1} (y)), ⟨“ N ”⟩ (T^{-1} (y) - \|T\|)) = T (T^{-1} (y))$
66	3	ad2antrr	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N)$
67		simpr	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to y \in (0 ..^N)$
68		f1ocnvfv2	$⊢ (T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N) \land y \in (0 ..^N)) \to T (T^{-1} (y)) = y$
69	66 67 68	syl2anc	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to T (T^{-1} (y)) = y$
70	65 69	eqtr2d	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to y = if (T^{-1} (y) \in (0 ..^\|T\|), T (T^{-1} (y)), ⟨“ N ”⟩ (T^{-1} (y) - \|T\|))$
71		simpr	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
72	30	adantr	$⊢ (φ \land x \in J) \to N \in ℤ_{\geq 0}$
73	72 33 36	syl2anc	$⊢ (φ \land x \in J) \to (x \in (0 ..^N) \lor x = N)$
74	73	ad5ant14	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to (x \in (0 ..^N) \lor x = N)$
75	67	ad3antrrr	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to y \in (0 ..^N)$
76	71	adantr	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
77		simpr	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to x = N$
78		fzonel	$⊢ \neg N \in (0 ..^N)$
79	78	a1i	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to \neg N \in (0 ..^N)$
80	63	eleq2i	$⊢ N \in (0 ..^N) \leftrightarrow N \in (0 ..^\|T\|)$
81	79 80	sylnib	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to \neg N \in (0 ..^\|T\|)$
82	77 81	eqneltrd	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to \neg x \in (0 ..^\|T\|)$
83	82	iffalsed	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = ⟨“ N ”⟩ (x - \|T\|)$
84	2 24	eqsstri	$⊢ J \subseteq ℕ_{0}$
85		simpllr	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to x \in J$
86	84 85	sselid	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to x \in ℕ_{0}$
87	86	nn0cnd	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to x \in ℂ$
88	77 1	eqtrdi	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to x = \|T\|$
89	87 88	subeq0bd	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to x - \|T\| = 0$
90	89	fveq2d	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to ⟨“ N ”⟩ (x - \|T\|) = ⟨“ N ”⟩ (0)$
91	46	ad5antr	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to ⟨“ N ”⟩ (0) = N$
92	90 91	eqtrd	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to ⟨“ N ”⟩ (x - \|T\|) = N$
93	76 83 92	3eqtrd	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to y = N$
94	93 79	eqneltrd	$⊢ (((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x = N) \to \neg y \in (0 ..^N)$
95	75 94	pm2.65da	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to \neg x = N$
96	74 95	olcnd	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to x \in (0 ..^N)$
97	96 63	eleqtrdi	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to x \in (0 ..^\|T\|)$
98	97	iftrued	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = T (x)$
99	71 98	eqtrd	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to y = T (x)$
100	99	fveq2d	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to T^{-1} (y) = T^{-1} (T (x))$
101	66	ad2antrr	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N)$
102		f1ocnvfv1	$⊢ (T : (0 ..^N) \underset{1-1 onto}{⟶} (0 ..^N) \land x \in (0 ..^N)) \to T^{-1} (T (x)) = x$
103	101 96 102	syl2anc	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to T^{-1} (T (x)) = x$
104	100 103	eqtr2d	$⊢ ((((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to x = T^{-1} (y)$
105	104	ex	$⊢ (((φ \land y \in J) \land y \in (0 ..^N)) \land x \in J) \to (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \to x = T^{-1} (y))$
106	105	ralrimiva	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to \forall x \in J (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \to x = T^{-1} (y))$
107		eleq1	$⊢ x = T^{-1} (y) \to (x \in (0 ..^\|T\|) \leftrightarrow T^{-1} (y) \in (0 ..^\|T\|))$
108		fveq2	$⊢ x = T^{-1} (y) \to T (x) = T (T^{-1} (y))$
109		fvoveq1	$⊢ x = T^{-1} (y) \to ⟨“ N ”⟩ (x - \|T\|) = ⟨“ N ”⟩ (T^{-1} (y) - \|T\|)$
110	107 108 109	ifbieq12d	$⊢ x = T^{-1} (y) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = if (T^{-1} (y) \in (0 ..^\|T\|), T (T^{-1} (y)), ⟨“ N ”⟩ (T^{-1} (y) - \|T\|))$
111	110	eqeq2d	$⊢ x = T^{-1} (y) \to (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \leftrightarrow y = if (T^{-1} (y) \in (0 ..^\|T\|), T (T^{-1} (y)), ⟨“ N ”⟩ (T^{-1} (y) - \|T\|)))$
112	111	eqreu	$⊢ (T^{-1} (y) \in J \land y = if (T^{-1} (y) \in (0 ..^\|T\|), T (T^{-1} (y)), ⟨“ N ”⟩ (T^{-1} (y) - \|T\|)) \land \forall x \in J (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \to x = T^{-1} (y))) \to \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
113	62 70 106 112	syl3anc	$⊢ ((φ \land y \in J) \land y \in (0 ..^N)) \to \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
114	51	ad2antrr	$⊢ ((φ \land y \in J) \land y = N) \to N \in J$
115	9	nn0cnd	$⊢ φ \to N \in ℂ$
116	115	ad2antrr	$⊢ ((φ \land y \in J) \land y = N) \to N \in ℂ$
117	1	a1i	$⊢ ((φ \land y \in J) \land y = N) \to N = \|T\|$
118	116 117	subeq0bd	$⊢ ((φ \land y \in J) \land y = N) \to N - \|T\| = 0$
119	118	fveq2d	$⊢ ((φ \land y \in J) \land y = N) \to ⟨“ N ”⟩ (N - \|T\|) = ⟨“ N ”⟩ (0)$
120	46	ad2antrr	$⊢ ((φ \land y \in J) \land y = N) \to ⟨“ N ”⟩ (0) = N$
121	119 120	eqtrd	$⊢ ((φ \land y \in J) \land y = N) \to ⟨“ N ”⟩ (N - \|T\|) = N$
122	78	a1i	$⊢ ((φ \land y \in J) \land y = N) \to \neg N \in (0 ..^N)$
123	122 80	sylnib	$⊢ ((φ \land y \in J) \land y = N) \to \neg N \in (0 ..^\|T\|)$
124	123	iffalsed	$⊢ ((φ \land y \in J) \land y = N) \to if (N \in (0 ..^\|T\|), T (N), ⟨“ N ”⟩ (N - \|T\|)) = ⟨“ N ”⟩ (N - \|T\|)$
125		simpr	$⊢ ((φ \land y \in J) \land y = N) \to y = N$
126	121 124 125	3eqtr4rd	$⊢ ((φ \land y \in J) \land y = N) \to y = if (N \in (0 ..^\|T\|), T (N), ⟨“ N ”⟩ (N - \|T\|))$
127	30	adantr	$⊢ (φ \land y \in J) \to N \in ℤ_{\geq 0}$
128	127	ad3antrrr	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to N \in ℤ_{\geq 0}$
129	33	ad5ant14	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to x \in (0 ..^N + 1)$
130	128 129 36	syl2anc	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to (x \in (0 ..^N) \lor x = N)$
131		simpr	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
132		simpllr	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to y = N$
133	131 132	eqtr3d	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = N$
134	133	adantr	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = N$
135	63	a1i	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to (0 ..^N) = (0 ..^\|T\|)$
136	135	eleq2d	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to (x \in (0 ..^N) \leftrightarrow x \in (0 ..^\|T\|))$
137	136	biimpa	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to x \in (0 ..^\|T\|)$
138	137	iftrued	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = T (x)$
139	5	ad4antr	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to T : (0 ..^N) ⟶ (0 ..^N)$
140	139	ffvelcdmda	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to T (x) \in (0 ..^N)$
141	138 140	eqeltrd	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \in (0 ..^N)$
142	134 141	eqeltrrd	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to N \in (0 ..^N)$
143	78	a1i	$⊢ (((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \land x \in (0 ..^N)) \to \neg N \in (0 ..^N)$
144	142 143	pm2.65da	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to \neg x \in (0 ..^N)$
145	130 144	orcnd	$⊢ ((((φ \land y \in J) \land y = N) \land x \in J) \land y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) \to x = N$
146	145	ex	$⊢ (((φ \land y \in J) \land y = N) \land x \in J) \to (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \to x = N)$
147	146	ralrimiva	$⊢ ((φ \land y \in J) \land y = N) \to \forall x \in J (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \to x = N)$
148		eleq1	$⊢ x = N \to (x \in (0 ..^\|T\|) \leftrightarrow N \in (0 ..^\|T\|))$
149		fveq2	$⊢ x = N \to T (x) = T (N)$
150		fvoveq1	$⊢ x = N \to ⟨“ N ”⟩ (x - \|T\|) = ⟨“ N ”⟩ (N - \|T\|)$
151	148 149 150	ifbieq12d	$⊢ x = N \to if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) = if (N \in (0 ..^\|T\|), T (N), ⟨“ N ”⟩ (N - \|T\|))$
152	151	eqeq2d	$⊢ x = N \to (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \leftrightarrow y = if (N \in (0 ..^\|T\|), T (N), ⟨“ N ”⟩ (N - \|T\|)))$
153	152	eqreu	$⊢ (N \in J \land y = if (N \in (0 ..^\|T\|), T (N), ⟨“ N ”⟩ (N - \|T\|)) \land \forall x \in J (y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \to x = N)) \to \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
154	114 126 147 153	syl3anc	$⊢ ((φ \land y \in J) \land y = N) \to \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
155	23	eleq2d	$⊢ φ \to (y \in J \leftrightarrow y \in (0 ..^N + 1))$
156	155	biimpa	$⊢ (φ \land y \in J) \to y \in (0 ..^N + 1)$
157		fzosplitsni	$⊢ N \in ℤ_{\geq 0} \to (y \in (0 ..^N + 1) \leftrightarrow (y \in (0 ..^N) \lor y = N))$
158	157	biimpa	$⊢ (N \in ℤ_{\geq 0} \land y \in (0 ..^N + 1)) \to (y \in (0 ..^N) \lor y = N)$
159	127 156 158	syl2anc	$⊢ (φ \land y \in J) \to (y \in (0 ..^N) \lor y = N)$
160	113 154 159	mpjaodan	$⊢ (φ \land y \in J) \to \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
161	160	ralrimiva	$⊢ φ \to \forall y \in J \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))$
162		s1len	$⊢ \|⟨“ N ”⟩\| = 1$
163	15 162	oveq12i	$⊢ \|T\| + \|⟨“ N ”⟩\| = N + 1$
164	163	oveq2i	$⊢ (0 ..^\|T\| + \|⟨“ N ”⟩\|) = (0 ..^N + 1)$
165	164 2	eqtr4i	$⊢ (0 ..^\|T\| + \|⟨“ N ”⟩\|) = J$
166	165	mpteq1i	$⊢ (x \in (0 ..^\|T\| + \|⟨“ N ”⟩\|) ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) = (x \in J ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)))$
167	166	f1ompt	$⊢ (x \in (0 ..^\|T\| + \|⟨“ N ”⟩\|) ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) : J \underset{1-1 onto}{⟶} J \leftrightarrow (\forall x \in J if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)) \in J \land \forall y \in J \exists! x \in J y = if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)))$
168	55 161 167	sylanbrc	$⊢ φ \to (x \in (0 ..^\|T\| + \|⟨“ N ”⟩\|) ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) : J \underset{1-1 onto}{⟶} J$
169		ovex	$⊢ (0 ..^N) \in V$
170		fex	$⊢ (T : (0 ..^N) ⟶ (0 ..^N) \land (0 ..^N) \in V) \to T \in V$
171	5 169 170	sylancl	$⊢ φ \to T \in V$
172		s1cli	$⊢ ⟨“ N ”⟩ \in Word V$
173		ccatfval	$⊢ (T \in V \land ⟨“ N ”⟩ \in Word V) \to T ++ ⟨“ N ”⟩ = (x \in (0 ..^\|T\| + \|⟨“ N ”⟩\|) ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)))$
174	171 172 173	sylancl	$⊢ φ \to T ++ ⟨“ N ”⟩ = (x \in (0 ..^\|T\| + \|⟨“ N ”⟩\|) ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|)))$
175	174	f1oeq1d	$⊢ φ \to ((T ++ ⟨“ N ”⟩) : J \underset{1-1 onto}{⟶} J \leftrightarrow (x \in (0 ..^\|T\| + \|⟨“ N ”⟩\|) ⟼ if (x \in (0 ..^\|T\|), T (x), ⟨“ N ”⟩ (x - \|T\|))) : J \underset{1-1 onto}{⟶} J)$
176	168 175	mpbird	$⊢ φ \to (T ++ ⟨“ N ”⟩) : J \underset{1-1 onto}{⟶} J$

Metamath Proof Explorer

Theorem ccatws1f1o

Proof