ccatf1

Description: Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023)

	Ref	Expression
Hypotheses	ccatf1.s	$⊢ φ \to S \in V$
	ccatf1.a	$⊢ φ \to A \in Word S$
	ccatf1.b	$⊢ φ \to B \in Word S$
	ccatf1.1	$⊢ φ \to A : dom A \underset{1-1}{⟶} S$
	ccatf1.2	$⊢ φ \to B : dom B \underset{1-1}{⟶} S$
	ccatf1.3	$⊢ φ \to ran A \cap ran B = \emptyset$
Assertion	ccatf1	$⊢ φ \to (A ++ B) : dom (A ++ B) \underset{1-1}{⟶} S$

Proof

Step	Hyp	Ref	Expression
1		ccatf1.s	$⊢ φ \to S \in V$
2		ccatf1.a	$⊢ φ \to A \in Word S$
3		ccatf1.b	$⊢ φ \to B \in Word S$
4		ccatf1.1	$⊢ φ \to A : dom A \underset{1-1}{⟶} S$
5		ccatf1.2	$⊢ φ \to B : dom B \underset{1-1}{⟶} S$
6		ccatf1.3	$⊢ φ \to ran A \cap ran B = \emptyset$
7		ccatcl	$⊢ (A \in Word S \land B \in Word S) \to A ++ B \in Word S$
8	2 3 7	syl2anc	$⊢ φ \to A ++ B \in Word S$
9		wrdf	$⊢ A ++ B \in Word S \to (A ++ B) : (0 ..^\|A ++ B\|) ⟶ S$
10	8 9	syl	$⊢ φ \to (A ++ B) : (0 ..^\|A ++ B\|) ⟶ S$
11	10	ffdmd	$⊢ φ \to (A ++ B) : dom (A ++ B) ⟶ S$
12		simpllr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to (A ++ B) (i) = (A ++ B) (j)$
13		id	$⊢ i \in (0 ..^\|A\|) \to i \in (0 ..^\|A\|)$
14		ccatval1	$⊢ (A \in Word S \land B \in Word S \land i \in (0 ..^\|A\|)) \to (A ++ B) (i) = A (i)$
15	2 3 13 14	syl2an3an	$⊢ (φ \land i \in (0 ..^\|A\|)) \to (A ++ B) (i) = A (i)$
16	15	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to (A ++ B) (i) = A (i)$
17		id	$⊢ j \in (0 ..^\|A\|) \to j \in (0 ..^\|A\|)$
18		ccatval1	$⊢ (A \in Word S \land B \in Word S \land j \in (0 ..^\|A\|)) \to (A ++ B) (j) = A (j)$
19	2 3 17 18	syl2an3an	$⊢ (φ \land j \in (0 ..^\|A\|)) \to (A ++ B) (j) = A (j)$
20	19	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to (A ++ B) (j) = A (j)$
21	12 16 20	3eqtr3d	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to A (i) = A (j)$
22		wrddm	$⊢ A \in Word S \to dom A = (0 ..^\|A\|)$
23	2 22	syl	$⊢ φ \to dom A = (0 ..^\|A\|)$
24		f1eq2	$⊢ dom A = (0 ..^\|A\|) \to (A : dom A \underset{1-1}{⟶} S \leftrightarrow A : (0 ..^\|A\|) \underset{1-1}{⟶} S)$
25	24	biimpa	$⊢ (dom A = (0 ..^\|A\|) \land A : dom A \underset{1-1}{⟶} S) \to A : (0 ..^\|A\|) \underset{1-1}{⟶} S$
26	23 4 25	syl2anc	$⊢ φ \to A : (0 ..^\|A\|) \underset{1-1}{⟶} S$
27		dff13	$⊢ A : (0 ..^\|A\|) \underset{1-1}{⟶} S \leftrightarrow (A : (0 ..^\|A\|) ⟶ S \land \forall i \in (0 ..^\|A\|) \forall j \in (0 ..^\|A\|) (A (i) = A (j) \to i = j))$
28	27	simprbi	$⊢ A : (0 ..^\|A\|) \underset{1-1}{⟶} S \to \forall i \in (0 ..^\|A\|) \forall j \in (0 ..^\|A\|) (A (i) = A (j) \to i = j)$
29	26 28	syl	$⊢ φ \to \forall i \in (0 ..^\|A\|) \forall j \in (0 ..^\|A\|) (A (i) = A (j) \to i = j)$
30	29	r19.21bi	$⊢ (φ \land i \in (0 ..^\|A\|)) \to \forall j \in (0 ..^\|A\|) (A (i) = A (j) \to i = j)$
31	30	r19.21bi	$⊢ ((φ \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to (A (i) = A (j) \to i = j)$
32	31	adantllr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to (A (i) = A (j) \to i = j)$
33	21 32	mpd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (0 ..^\|A\|)) \to i = j$
34	33	ex	$⊢ ((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \to (j \in (0 ..^\|A\|) \to i = j)$
35	34	adantllr	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \to (j \in (0 ..^\|A\|) \to i = j)$
36		f1fun	$⊢ A : dom A \underset{1-1}{⟶} S \to Fun A$
37	4 36	syl	$⊢ φ \to Fun A$
38		simpr	$⊢ (φ \land i \in (0 ..^\|A\|)) \to i \in (0 ..^\|A\|)$
39	23	adantr	$⊢ (φ \land i \in (0 ..^\|A\|)) \to dom A = (0 ..^\|A\|)$
40	38 39	eleqtrrd	$⊢ (φ \land i \in (0 ..^\|A\|)) \to i \in dom A$
41		fvelrn	$⊢ (Fun A \land i \in dom A) \to A (i) \in ran A$
42	37 40 41	syl2an2r	$⊢ (φ \land i \in (0 ..^\|A\|)) \to A (i) \in ran A$
43	42	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to A (i) \in ran A$
44		simpllr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (i) = (A ++ B) (j)$
45	15	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (i) = A (i)$
46	2	adantr	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to A \in Word S$
47	3	adantr	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to B \in Word S$
48		simpr	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to j \in (\|A\| ..^\|A ++ B\|)$
49		ccatlen	$⊢ (A \in Word S \land B \in Word S) \to \|A ++ B\| = \|A\| + \|B\|$
50	2 3 49	syl2anc	$⊢ φ \to \|A ++ B\| = \|A\| + \|B\|$
51	50	oveq2d	$⊢ φ \to (\|A\| ..^\|A ++ B\|) = (\|A\| ..^\|A\| + \|B\|)$
52	51	adantr	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to (\|A\| ..^\|A ++ B\|) = (\|A\| ..^\|A\| + \|B\|)$
53	48 52	eleqtrd	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to j \in (\|A\| ..^\|A\| + \|B\|)$
54		ccatval2	$⊢ (A \in Word S \land B \in Word S \land j \in (\|A\| ..^\|A\| + \|B\|)) \to (A ++ B) (j) = B (j - \|A\|)$
55	46 47 53 54	syl3anc	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (j) = B (j - \|A\|)$
56	55	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (j) = B (j - \|A\|)$
57	44 45 56	3eqtr3d	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to A (i) = B (j - \|A\|)$
58		f1fun	$⊢ B : dom B \underset{1-1}{⟶} S \to Fun B$
59	5 58	syl	$⊢ φ \to Fun B$
60		lencl	$⊢ B \in Word S \to \|B\| \in ℕ_{0}$
61	3 60	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
62	61	nn0zd	$⊢ φ \to \|B\| \in ℤ$
63	62	adantr	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to \|B\| \in ℤ$
64		fzosubel3	$⊢ (j \in (\|A\| ..^\|A\| + \|B\|) \land \|B\| \in ℤ) \to j - \|A\| \in (0 ..^\|B\|)$
65	53 63 64	syl2anc	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to j - \|A\| \in (0 ..^\|B\|)$
66		wrddm	$⊢ B \in Word S \to dom B = (0 ..^\|B\|)$
67	3 66	syl	$⊢ φ \to dom B = (0 ..^\|B\|)$
68	67	adantr	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to dom B = (0 ..^\|B\|)$
69	65 68	eleqtrrd	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to j - \|A\| \in dom B$
70		fvelrn	$⊢ (Fun B \land j - \|A\| \in dom B) \to B (j - \|A\|) \in ran B$
71	59 69 70	syl2an2r	$⊢ (φ \land j \in (\|A\| ..^\|A ++ B\|)) \to B (j - \|A\|) \in ran B$
72	71	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to B (j - \|A\|) \in ran B$
73	57 72	eqeltrd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to A (i) \in ran B$
74	43 73	elind	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to A (i) \in (ran A \cap ran B)$
75	6	ad3antrrr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to ran A \cap ran B = \emptyset$
76	74 75	eleqtrd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to A (i) \in \emptyset$
77		noel	$⊢ \neg A (i) \in \emptyset$
78	77	a1i	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to \neg A (i) \in \emptyset$
79	76 78	pm2.21dd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to i = j$
80	79	ex	$⊢ ((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \to (j \in (\|A\| ..^\|A ++ B\|) \to i = j)$
81	80	adantllr	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \to (j \in (\|A\| ..^\|A ++ B\|) \to i = j)$
82		wrddm	$⊢ A ++ B \in Word S \to dom (A ++ B) = (0 ..^\|A ++ B\|)$
83	8 82	syl	$⊢ φ \to dom (A ++ B) = (0 ..^\|A ++ B\|)$
84	83	eleq2d	$⊢ φ \to (j \in dom (A ++ B) \leftrightarrow j \in (0 ..^\|A ++ B\|))$
85	84	biimpa	$⊢ (φ \land j \in dom (A ++ B)) \to j \in (0 ..^\|A ++ B\|)$
86		lencl	$⊢ A \in Word S \to \|A\| \in ℕ_{0}$
87	2 86	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
88	87	nn0zd	$⊢ φ \to \|A\| \in ℤ$
89	88	adantr	$⊢ (φ \land j \in dom (A ++ B)) \to \|A\| \in ℤ$
90		fzospliti	$⊢ (j \in (0 ..^\|A ++ B\|) \land \|A\| \in ℤ) \to (j \in (0 ..^\|A\|) \lor j \in (\|A\| ..^\|A ++ B\|))$
91	85 89 90	syl2anc	$⊢ (φ \land j \in dom (A ++ B)) \to (j \in (0 ..^\|A\|) \lor j \in (\|A\| ..^\|A ++ B\|))$
92	91	ad2antrr	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \to (j \in (0 ..^\|A\|) \lor j \in (\|A\| ..^\|A ++ B\|))$
93	35 81 92	mpjaod	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (0 ..^\|A\|)) \to i = j$
94	93	ex	$⊢ ((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \to (i \in (0 ..^\|A\|) \to i = j)$
95	94	adantlrl	$⊢ ((φ \land (i \in dom (A ++ B) \land j \in dom (A ++ B))) \land (A ++ B) (i) = (A ++ B) (j)) \to (i \in (0 ..^\|A\|) \to i = j)$
96		simpr	$⊢ (φ \land j \in (0 ..^\|A\|)) \to j \in (0 ..^\|A\|)$
97	23	adantr	$⊢ (φ \land j \in (0 ..^\|A\|)) \to dom A = (0 ..^\|A\|)$
98	96 97	eleqtrrd	$⊢ (φ \land j \in (0 ..^\|A\|)) \to j \in dom A$
99		fvelrn	$⊢ (Fun A \land j \in dom A) \to A (j) \in ran A$
100	37 98 99	syl2an2r	$⊢ (φ \land j \in (0 ..^\|A\|)) \to A (j) \in ran A$
101	100	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to A (j) \in ran A$
102		simpllr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to (A ++ B) (i) = (A ++ B) (j)$
103	2	adantr	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to A \in Word S$
104	3	adantr	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to B \in Word S$
105		simpr	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to i \in (\|A\| ..^\|A ++ B\|)$
106	51	adantr	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to (\|A\| ..^\|A ++ B\|) = (\|A\| ..^\|A\| + \|B\|)$
107	105 106	eleqtrd	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to i \in (\|A\| ..^\|A\| + \|B\|)$
108		ccatval2	$⊢ (A \in Word S \land B \in Word S \land i \in (\|A\| ..^\|A\| + \|B\|)) \to (A ++ B) (i) = B (i - \|A\|)$
109	103 104 107 108	syl3anc	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (i) = B (i - \|A\|)$
110	109	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to (A ++ B) (i) = B (i - \|A\|)$
111	19	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to (A ++ B) (j) = A (j)$
112	102 110 111	3eqtr3rd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to A (j) = B (i - \|A\|)$
113	62	adantr	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to \|B\| \in ℤ$
114		fzosubel3	$⊢ (i \in (\|A\| ..^\|A\| + \|B\|) \land \|B\| \in ℤ) \to i - \|A\| \in (0 ..^\|B\|)$
115	107 113 114	syl2anc	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to i - \|A\| \in (0 ..^\|B\|)$
116	67	adantr	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to dom B = (0 ..^\|B\|)$
117	115 116	eleqtrrd	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to i - \|A\| \in dom B$
118		fvelrn	$⊢ (Fun B \land i - \|A\| \in dom B) \to B (i - \|A\|) \in ran B$
119	59 117 118	syl2an2r	$⊢ (φ \land i \in (\|A\| ..^\|A ++ B\|)) \to B (i - \|A\|) \in ran B$
120	119	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to B (i - \|A\|) \in ran B$
121	112 120	eqeltrd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to A (j) \in ran B$
122	101 121	elind	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to A (j) \in (ran A \cap ran B)$
123	6	ad3antrrr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to ran A \cap ran B = \emptyset$
124	122 123	eleqtrd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to A (j) \in \emptyset$
125		noel	$⊢ \neg A (j) \in \emptyset$
126	125	a1i	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to \neg A (j) \in \emptyset$
127	124 126	pm2.21dd	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (0 ..^\|A\|)) \to i = j$
128	127	ex	$⊢ ((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \to (j \in (0 ..^\|A\|) \to i = j)$
129	128	adantllr	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \to (j \in (0 ..^\|A\|) \to i = j)$
130		elfzoelz	$⊢ i \in (\|A\| ..^\|A ++ B\|) \to i \in ℤ$
131	130	zcnd	$⊢ i \in (\|A\| ..^\|A ++ B\|) \to i \in ℂ$
132	131	ad2antlr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to i \in ℂ$
133		elfzoelz	$⊢ j \in (\|A\| ..^\|A ++ B\|) \to j \in ℤ$
134	133	zcnd	$⊢ j \in (\|A\| ..^\|A ++ B\|) \to j \in ℂ$
135	134	adantl	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to j \in ℂ$
136	87	nn0cnd	$⊢ φ \to \|A\| \in ℂ$
137	136	ad3antrrr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to \|A\| \in ℂ$
138	5	ad3antrrr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to B : dom B \underset{1-1}{⟶} S$
139	117	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to i - \|A\| \in dom B$
140	69	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to j - \|A\| \in dom B$
141	139 140	jca	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (i - \|A\| \in dom B \land j - \|A\| \in dom B)$
142		simpllr	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (i) = (A ++ B) (j)$
143	109	ad4ant13	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (i) = B (i - \|A\|)$
144	55	ad4ant14	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to (A ++ B) (j) = B (j - \|A\|)$
145	142 143 144	3eqtr3d	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to B (i - \|A\|) = B (j - \|A\|)$
146		f1veqaeq	$⊢ (B : dom B \underset{1-1}{⟶} S \land (i - \|A\| \in dom B \land j - \|A\| \in dom B)) \to (B (i - \|A\|) = B (j - \|A\|) \to i - \|A\| = j - \|A\|)$
147	146	imp	$⊢ ((B : dom B \underset{1-1}{⟶} S \land (i - \|A\| \in dom B \land j - \|A\| \in dom B)) \land B (i - \|A\|) = B (j - \|A\|)) \to i - \|A\| = j - \|A\|$
148	138 141 145 147	syl21anc	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to i - \|A\| = j - \|A\|$
149	132 135 137 148	subcan2d	$⊢ (((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \land j \in (\|A\| ..^\|A ++ B\|)) \to i = j$
150	149	ex	$⊢ ((φ \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \to (j \in (\|A\| ..^\|A ++ B\|) \to i = j)$
151	150	adantllr	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \to (j \in (\|A\| ..^\|A ++ B\|) \to i = j)$
152	91	ad2antrr	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \to (j \in (0 ..^\|A\|) \lor j \in (\|A\| ..^\|A ++ B\|))$
153	129 151 152	mpjaod	$⊢ (((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \land i \in (\|A\| ..^\|A ++ B\|)) \to i = j$
154	153	ex	$⊢ ((φ \land j \in dom (A ++ B)) \land (A ++ B) (i) = (A ++ B) (j)) \to (i \in (\|A\| ..^\|A ++ B\|) \to i = j)$
155	154	adantlrl	$⊢ ((φ \land (i \in dom (A ++ B) \land j \in dom (A ++ B))) \land (A ++ B) (i) = (A ++ B) (j)) \to (i \in (\|A\| ..^\|A ++ B\|) \to i = j)$
156	83	eleq2d	$⊢ φ \to (i \in dom (A ++ B) \leftrightarrow i \in (0 ..^\|A ++ B\|))$
157	156	biimpa	$⊢ (φ \land i \in dom (A ++ B)) \to i \in (0 ..^\|A ++ B\|)$
158	88	adantr	$⊢ (φ \land i \in dom (A ++ B)) \to \|A\| \in ℤ$
159		fzospliti	$⊢ (i \in (0 ..^\|A ++ B\|) \land \|A\| \in ℤ) \to (i \in (0 ..^\|A\|) \lor i \in (\|A\| ..^\|A ++ B\|))$
160	157 158 159	syl2anc	$⊢ (φ \land i \in dom (A ++ B)) \to (i \in (0 ..^\|A\|) \lor i \in (\|A\| ..^\|A ++ B\|))$
161	160	adantrr	$⊢ (φ \land (i \in dom (A ++ B) \land j \in dom (A ++ B))) \to (i \in (0 ..^\|A\|) \lor i \in (\|A\| ..^\|A ++ B\|))$
162	161	adantr	$⊢ ((φ \land (i \in dom (A ++ B) \land j \in dom (A ++ B))) \land (A ++ B) (i) = (A ++ B) (j)) \to (i \in (0 ..^\|A\|) \lor i \in (\|A\| ..^\|A ++ B\|))$
163	95 155 162	mpjaod	$⊢ ((φ \land (i \in dom (A ++ B) \land j \in dom (A ++ B))) \land (A ++ B) (i) = (A ++ B) (j)) \to i = j$
164	163	ex	$⊢ (φ \land (i \in dom (A ++ B) \land j \in dom (A ++ B))) \to ((A ++ B) (i) = (A ++ B) (j) \to i = j)$
165	164	ralrimivva	$⊢ φ \to \forall i \in dom (A ++ B) \forall j \in dom (A ++ B) ((A ++ B) (i) = (A ++ B) (j) \to i = j)$
166		dff13	$⊢ (A ++ B) : dom (A ++ B) \underset{1-1}{⟶} S \leftrightarrow ((A ++ B) : dom (A ++ B) ⟶ S \land \forall i \in dom (A ++ B) \forall j \in dom (A ++ B) ((A ++ B) (i) = (A ++ B) (j) \to i = j))$
167	11 165 166	sylanbrc	$⊢ φ \to (A ++ B) : dom (A ++ B) \underset{1-1}{⟶} S$

Metamath Proof Explorer

Theorem ccatf1

Proof