s3f1

Description: Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023)

	Ref	Expression
Hypotheses	s3f1.i	$⊢ φ \to I \in D$
	s3f1.j	$⊢ φ \to J \in D$
	s3f1.k	$⊢ φ \to K \in D$
	s3f1.1	$⊢ φ \to I \neq J$
	s3f1.2	$⊢ φ \to J \neq K$
	s3f1.3	$⊢ φ \to K \neq I$
Assertion	s3f1	$⊢ φ \to ⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ \underset{1-1}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		s3f1.i	$⊢ φ \to I \in D$
2		s3f1.j	$⊢ φ \to J \in D$
3		s3f1.k	$⊢ φ \to K \in D$
4		s3f1.1	$⊢ φ \to I \neq J$
5		s3f1.2	$⊢ φ \to J \neq K$
6		s3f1.3	$⊢ φ \to K \neq I$
7	1 2 3	s3cld	$⊢ φ \to ⟨“ I J K ”⟩ \in Word D$
8		wrdf	$⊢ ⟨“ I J K ”⟩ \in Word D \to ⟨“ I J K ”⟩ : (0 ..^\|⟨“ I J K ”⟩\|) ⟶ D$
9	7 8	syl	$⊢ φ \to ⟨“ I J K ”⟩ : (0 ..^\|⟨“ I J K ”⟩\|) ⟶ D$
10	9	ffdmd	$⊢ φ \to ⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ ⟶ D$
11		simplr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 0) \to i = 0$
12		simpr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 0) \to j = 0$
13	11 12	eqtr4d	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 0) \to i = j$
14		simpllr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 1) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)$
15		simpr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \to i = 0$
16	15	fveq2d	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (0)$
17		s3fv0	$⊢ I \in D \to ⟨“ I J K ”⟩ (0) = I$
18	1 17	syl	$⊢ φ \to ⟨“ I J K ”⟩ (0) = I$
19	18	ad4antr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \to ⟨“ I J K ”⟩ (0) = I$
20	16 19	eqtrd	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \to ⟨“ I J K ”⟩ (i) = I$
21	20	adantr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 1) \to ⟨“ I J K ”⟩ (i) = I$
22		simpr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 1) \to j = 1$
23	22	fveq2d	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 1) \to ⟨“ I J K ”⟩ (j) = ⟨“ I J K ”⟩ (1)$
24		s3fv1	$⊢ J \in D \to ⟨“ I J K ”⟩ (1) = J$
25	2 24	syl	$⊢ φ \to ⟨“ I J K ”⟩ (1) = J$
26	25	ad4antr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 1) \to ⟨“ I J K ”⟩ (1) = J$
27	23 26	eqtrd	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 1) \to ⟨“ I J K ”⟩ (j) = J$
28	27	adantlr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 1) \to ⟨“ I J K ”⟩ (j) = J$
29	14 21 28	3eqtr3d	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 1) \to I = J$
30	4	ad5antr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 1) \to I \neq J$
31	29 30	pm2.21ddne	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 1) \to i = j$
32		simpllr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 2) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)$
33	20	adantr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 2) \to ⟨“ I J K ”⟩ (i) = I$
34		simpr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 2) \to j = 2$
35	34	fveq2d	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 2) \to ⟨“ I J K ”⟩ (j) = ⟨“ I J K ”⟩ (2)$
36		s3fv2	$⊢ K \in D \to ⟨“ I J K ”⟩ (2) = K$
37	3 36	syl	$⊢ φ \to ⟨“ I J K ”⟩ (2) = K$
38	37	ad4antr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 2) \to ⟨“ I J K ”⟩ (2) = K$
39	35 38	eqtrd	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 2) \to ⟨“ I J K ”⟩ (j) = K$
40	39	adantlr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 2) \to ⟨“ I J K ”⟩ (j) = K$
41	32 33 40	3eqtr3rd	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 2) \to K = I$
42	6	ad5antr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 2) \to K \neq I$
43	41 42	pm2.21ddne	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \land j = 2) \to i = j$
44		wrddm	$⊢ ⟨“ I J K ”⟩ \in Word D \to dom ⟨“ I J K ”⟩ = (0 ..^\|⟨“ I J K ”⟩\|)$
45	7 44	syl	$⊢ φ \to dom ⟨“ I J K ”⟩ = (0 ..^\|⟨“ I J K ”⟩\|)$
46		s3len	$⊢ \|⟨“ I J K ”⟩\| = 3$
47	46	oveq2i	$⊢ (0 ..^\|⟨“ I J K ”⟩\|) = (0 ..^3)$
48		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
49	47 48	eqtri	$⊢ (0 ..^\|⟨“ I J K ”⟩\|) = \{0, 1, 2\}$
50	45 49	eqtrdi	$⊢ φ \to dom ⟨“ I J K ”⟩ = \{0, 1, 2\}$
51	50	eleq2d	$⊢ φ \to (j \in dom ⟨“ I J K ”⟩ \leftrightarrow j \in \{0, 1, 2\})$
52	51	biimpa	$⊢ (φ \land j \in dom ⟨“ I J K ”⟩) \to j \in \{0, 1, 2\}$
53		vex	$⊢ j \in V$
54	53	eltp	$⊢ j \in \{0, 1, 2\} \leftrightarrow (j = 0 \lor j = 1 \lor j = 2)$
55	52 54	sylib	$⊢ (φ \land j \in dom ⟨“ I J K ”⟩) \to (j = 0 \lor j = 1 \lor j = 2)$
56	55	adantlr	$⊢ ((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \to (j = 0 \lor j = 1 \lor j = 2)$
57	56	ad2antrr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \to (j = 0 \lor j = 1 \lor j = 2)$
58	13 31 43 57	mpjao3dan	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 0) \to i = j$
59		simpllr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 0) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)$
60		simpr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \to i = 1$
61	60	fveq2d	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (1)$
62	25	ad4antr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \to ⟨“ I J K ”⟩ (1) = J$
63	61 62	eqtrd	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \to ⟨“ I J K ”⟩ (i) = J$
64	63	adantr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 0) \to ⟨“ I J K ”⟩ (i) = J$
65		simpr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 0) \to j = 0$
66	65	fveq2d	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 0) \to ⟨“ I J K ”⟩ (j) = ⟨“ I J K ”⟩ (0)$
67	18	ad4antr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 0) \to ⟨“ I J K ”⟩ (0) = I$
68	66 67	eqtrd	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land j = 0) \to ⟨“ I J K ”⟩ (j) = I$
69	68	adantlr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 0) \to ⟨“ I J K ”⟩ (j) = I$
70	59 64 69	3eqtr3rd	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 0) \to I = J$
71	4	ad5antr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 0) \to I \neq J$
72	70 71	pm2.21ddne	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 0) \to i = j$
73		simplr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 1) \to i = 1$
74		simpr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 1) \to j = 1$
75	73 74	eqtr4d	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 1) \to i = j$
76		simpllr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 2) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)$
77	63	adantr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 2) \to ⟨“ I J K ”⟩ (i) = J$
78	39	adantlr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 2) \to ⟨“ I J K ”⟩ (j) = K$
79	76 77 78	3eqtr3d	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 2) \to J = K$
80	5	ad5antr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 2) \to J \neq K$
81	79 80	pm2.21ddne	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \land j = 2) \to i = j$
82	56	ad2antrr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \to (j = 0 \lor j = 1 \lor j = 2)$
83	72 75 81 82	mpjao3dan	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 1) \to i = j$
84		simpllr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 0) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)$
85		simpr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \to i = 2$
86	85	fveq2d	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (2)$
87	37	ad4antr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \to ⟨“ I J K ”⟩ (2) = K$
88	86 87	eqtrd	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \to ⟨“ I J K ”⟩ (i) = K$
89	88	adantr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 0) \to ⟨“ I J K ”⟩ (i) = K$
90	68	adantlr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 0) \to ⟨“ I J K ”⟩ (j) = I$
91	84 89 90	3eqtr3d	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 0) \to K = I$
92	6	ad5antr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 0) \to K \neq I$
93	91 92	pm2.21ddne	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 0) \to i = j$
94		simpllr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 1) \to ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)$
95	88	adantr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 1) \to ⟨“ I J K ”⟩ (i) = K$
96	27	adantlr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 1) \to ⟨“ I J K ”⟩ (j) = J$
97	94 95 96	3eqtr3rd	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 1) \to J = K$
98	5	ad5antr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 1) \to J \neq K$
99	97 98	pm2.21ddne	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 1) \to i = j$
100		simplr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 2) \to i = 2$
101		simpr	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 2) \to j = 2$
102	100 101	eqtr4d	$⊢ (((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \land j = 2) \to i = j$
103	56	ad2antrr	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \to (j = 0 \lor j = 1 \lor j = 2)$
104	93 99 102 103	mpjao3dan	$⊢ ((((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \land i = 2) \to i = j$
105	50	eleq2d	$⊢ φ \to (i \in dom ⟨“ I J K ”⟩ \leftrightarrow i \in \{0, 1, 2\})$
106	105	biimpa	$⊢ (φ \land i \in dom ⟨“ I J K ”⟩) \to i \in \{0, 1, 2\}$
107		vex	$⊢ i \in V$
108	107	eltp	$⊢ i \in \{0, 1, 2\} \leftrightarrow (i = 0 \lor i = 1 \lor i = 2)$
109	106 108	sylib	$⊢ (φ \land i \in dom ⟨“ I J K ”⟩) \to (i = 0 \lor i = 1 \lor i = 2)$
110	109	ad2antrr	$⊢ (((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \to (i = 0 \lor i = 1 \lor i = 2)$
111	58 83 104 110	mpjao3dan	$⊢ (((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \land ⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j)) \to i = j$
112	111	ex	$⊢ ((φ \land i \in dom ⟨“ I J K ”⟩) \land j \in dom ⟨“ I J K ”⟩) \to (⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j) \to i = j)$
113	112	anasss	$⊢ (φ \land (i \in dom ⟨“ I J K ”⟩ \land j \in dom ⟨“ I J K ”⟩)) \to (⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j) \to i = j)$
114	113	ralrimivva	$⊢ φ \to \forall i \in dom ⟨“ I J K ”⟩ \forall j \in dom ⟨“ I J K ”⟩ (⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j) \to i = j)$
115		dff13	$⊢ ⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ \underset{1-1}{⟶} D \leftrightarrow (⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ ⟶ D \land \forall i \in dom ⟨“ I J K ”⟩ \forall j \in dom ⟨“ I J K ”⟩ (⟨“ I J K ”⟩ (i) = ⟨“ I J K ”⟩ (j) \to i = j))$
116	10 114 115	sylanbrc	$⊢ φ \to ⟨“ I J K ”⟩ : dom ⟨“ I J K ”⟩ \underset{1-1}{⟶} D$

Metamath Proof Explorer

Theorem s3f1

Proof