fvf1tp

Description: Values of a one-to-one function between two sets with three elements. Actually, such a function is a bijection. (Contributed by AV, 23-Jul-2025)

		Ref	Expression
	Assertion	fvf1tp	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to F : (0 ..^3) ⟶ \{X, Y, Z\}$
2		3nn	$⊢ 3 \in ℕ$
3		lbfzo0	$⊢ 0 \in (0 ..^3) \leftrightarrow 3 \in ℕ$
4	2 3	mpbir	$⊢ 0 \in (0 ..^3)$
5	4	a1i	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to 0 \in (0 ..^3)$
6	1 5	ffvelcdmd	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to F (0) \in \{X, Y, Z\}$
7		1nn0	$⊢ 1 \in ℕ_{0}$
8		1lt3	$⊢ 1 < 3$
9		elfzo0	$⊢ 1 \in (0 ..^3) \leftrightarrow (1 \in ℕ_{0} \land 3 \in ℕ \land 1 < 3)$
10	7 2 8 9	mpbir3an	$⊢ 1 \in (0 ..^3)$
11	10	a1i	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to 1 \in (0 ..^3)$
12	1 11	ffvelcdmd	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to F (1) \in \{X, Y, Z\}$
13		2nn0	$⊢ 2 \in ℕ_{0}$
14		2lt3	$⊢ 2 < 3$
15		elfzo0	$⊢ 2 \in (0 ..^3) \leftrightarrow (2 \in ℕ_{0} \land 3 \in ℕ \land 2 < 3)$
16	13 2 14 15	mpbir3an	$⊢ 2 \in (0 ..^3)$
17	16	a1i	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to 2 \in (0 ..^3)$
18	1 17	ffvelcdmd	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to F (2) \in \{X, Y, Z\}$
19		eltpi	$⊢ F (0) \in \{X, Y, Z\} \to (F (0) = X \lor F (0) = Y \lor F (0) = Z)$
20		eltpi	$⊢ F (1) \in \{X, Y, Z\} \to (F (1) = X \lor F (1) = Y \lor F (1) = Z)$
21		eltpi	$⊢ F (2) \in \{X, Y, Z\} \to (F (2) = X \lor F (2) = Y \lor F (2) = Z)$
22	19 20 21	3anim123i	$⊢ (F (0) \in \{X, Y, Z\} \land F (1) \in \{X, Y, Z\} \land F (2) \in \{X, Y, Z\}) \to ((F (0) = X \lor F (0) = Y \lor F (0) = Z) \land (F (1) = X \lor F (1) = Y \lor F (1) = Z) \land (F (2) = X \lor F (2) = Y \lor F (2) = Z))$
23		eqeq2	$⊢ X = F (0) \to (F (1) = X \leftrightarrow F (1) = F (0))$
24	23	eqcoms	$⊢ F (0) = X \to (F (1) = X \leftrightarrow F (1) = F (0))$
25	24	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (1) = X \leftrightarrow F (1) = F (0))$
26		f1veqaeq	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land (1 \in (0 ..^3) \land 0 \in (0 ..^3))) \to (F (1) = F (0) \to 1 = 0)$
27	10 4 26	mpanr12	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (1) = F (0) \to 1 = 0)$
28		ax-1ne0	$⊢ 1 \neq 0$
29		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
30	27 28 29	syl6mpi	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (1) = F (0) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
31	30	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (1) = F (0) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
32	25 31	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (1) = X \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
33		eqeq2	$⊢ X = F (0) \to (F (2) = X \leftrightarrow F (2) = F (0))$
34	33	eqcoms	$⊢ F (0) = X \to (F (2) = X \leftrightarrow F (2) = F (0))$
35	34	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = X \leftrightarrow F (2) = F (0))$
36	16 4	pm3.2i	$⊢ (2 \in (0 ..^3) \land 0 \in (0 ..^3))$
37	36	a1i	$⊢ F (0) = X \to (2 \in (0 ..^3) \land 0 \in (0 ..^3))$
38		f1veqaeq	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land (2 \in (0 ..^3) \land 0 \in (0 ..^3))) \to (F (2) = F (0) \to 2 = 0)$
39	37 38	sylan2	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = F (0) \to 2 = 0)$
40		2ne0	$⊢ 2 \neq 0$
41		eqneqall	$⊢ 2 = 0 \to (2 \neq 0 \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
42	39 40 41	syl6mpi	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = F (0) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
43	35 42	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
44	43	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
45		eqeq2	$⊢ Y = F (1) \to (F (2) = Y \leftrightarrow F (2) = F (1))$
46	45	eqcoms	$⊢ F (1) = Y \to (F (2) = Y \leftrightarrow F (2) = F (1))$
47	46	adantl	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \to (F (2) = Y \leftrightarrow F (2) = F (1))$
48	16 10	pm3.2i	$⊢ (2 \in (0 ..^3) \land 1 \in (0 ..^3))$
49	48	a1i	$⊢ F (0) = X \to (2 \in (0 ..^3) \land 1 \in (0 ..^3))$
50		f1veqaeq	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land (2 \in (0 ..^3) \land 1 \in (0 ..^3))) \to (F (2) = F (1) \to 2 = 1)$
51	49 50	sylan2	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = F (1) \to 2 = 1)$
52		1ne2	$⊢ 1 \neq 2$
53	52	necomi	$⊢ 2 \neq 1$
54		eqneqall	$⊢ 2 = 1 \to (2 \neq 1 \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
55	51 53 54	syl6mpi	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
56	55	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
57	47 56	sylbid	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
58		simpllr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \land F (2) = Z) \to F (0) = X$
59		simplr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \land F (2) = Z) \to F (1) = Y$
60		simpr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \land F (2) = Z) \to F (2) = Z$
61	58 59 60	3jca	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \land F (2) = Z) \to (F (0) = X \land F (1) = Y \land F (2) = Z)$
62	61	orcd	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \land F (2) = Z) \to ((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y))$
63	62	3mix1d	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \land F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$
64	63	ex	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
65	44 57 64	3jaod	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Y) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
66	65	ex	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (1) = Y \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
67	43	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
68		simpllr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \land F (2) = Y) \to F (0) = X$
69		simplr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \land F (2) = Y) \to F (1) = Z$
70		simpr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \land F (2) = Y) \to F (2) = Y$
71	68 69 70	3jca	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \land F (2) = Y) \to (F (0) = X \land F (1) = Z \land F (2) = Y)$
72	71	olcd	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \land F (2) = Y) \to ((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y))$
73	72	3mix1d	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \land F (2) = Y) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$
74	73	ex	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
75		eqeq2	$⊢ Z = F (1) \to (F (2) = Z \leftrightarrow F (2) = F (1))$
76	75	eqcoms	$⊢ F (1) = Z \to (F (2) = Z \leftrightarrow F (2) = F (1))$
77	76	adantl	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \to (F (2) = Z \leftrightarrow F (2) = F (1))$
78	16 10 50	mpanr12	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (2) = F (1) \to 2 = 1)$
79	78 53 54	syl6mpi	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
80	79	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
81	80	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
82	77 81	sylbid	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
83	67 74 82	3jaod	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \land F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
84	83	ex	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to (F (1) = Z \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
85	32 66 84	3jaod	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = X) \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
86	85	ex	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (0) = X \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))))$
87		eqeq2	$⊢ X = F (1) \to (F (2) = X \leftrightarrow F (2) = F (1))$
88	87	eqcoms	$⊢ F (1) = X \to (F (2) = X \leftrightarrow F (2) = F (1))$
89	88	adantl	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \to (F (2) = X \leftrightarrow F (2) = F (1))$
90	79	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
91	90	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
92	89 91	sylbid	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
93		eqeq2	$⊢ Y = F (0) \to (F (2) = Y \leftrightarrow F (2) = F (0))$
94	93	eqcoms	$⊢ F (0) = Y \to (F (2) = Y \leftrightarrow F (2) = F (0))$
95	94	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (2) = Y \leftrightarrow F (2) = F (0))$
96	16 4 38	mpanr12	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (2) = F (0) \to 2 = 0)$
97	96 40 41	syl6mpi	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (2) = F (0) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
98	97	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (2) = F (0) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
99	95 98	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
100	99	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
101		simpllr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \land F (2) = Z) \to F (0) = Y$
102		simplr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \land F (2) = Z) \to F (1) = X$
103		simpr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \land F (2) = Z) \to F (2) = Z$
104	101 102 103	3jca	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \land F (2) = Z) \to (F (0) = Y \land F (1) = X \land F (2) = Z)$
105	104	orcd	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \land F (2) = Z) \to ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X))$
106	105	3mix2d	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \land F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$
107	106	ex	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
108	92 100 107	3jaod	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = X) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
109	108	ex	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (1) = X \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
110		eqeq2	$⊢ Y = F (0) \to (F (1) = Y \leftrightarrow F (1) = F (0))$
111	110	eqcoms	$⊢ F (0) = Y \to (F (1) = Y \leftrightarrow F (1) = F (0))$
112	111	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (1) = Y \leftrightarrow F (1) = F (0))$
113	30	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (1) = F (0) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
114	112 113	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (1) = Y \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
115		simpllr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \land F (2) = X) \to F (0) = Y$
116		simplr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \land F (2) = X) \to F (1) = Z$
117		simpr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \land F (2) = X) \to F (2) = X$
118	115 116 117	3jca	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \land F (2) = X) \to (F (0) = Y \land F (1) = Z \land F (2) = X)$
119	118	olcd	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \land F (2) = X) \to ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X))$
120	119	3mix2d	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \land F (2) = X) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$
121	120	ex	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
122	99	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
123	76	adantl	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \to (F (2) = Z \leftrightarrow F (2) = F (1))$
124	90	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
125	123 124	sylbid	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
126	121 122 125	3jaod	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \land F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
127	126	ex	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to (F (1) = Z \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
128	109 114 127	3jaod	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Y) \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
129	128	ex	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (0) = Y \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))))$
130	88	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (1) = X) \to (F (2) = X \leftrightarrow F (2) = F (1))$
131	79	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (1) = X) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
132	130 131	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (1) = X) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
133	132	adantlr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
134		simpllr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \land F (2) = Y) \to F (0) = Z$
135		simplr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \land F (2) = Y) \to F (1) = X$
136		simpr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \land F (2) = Y) \to F (2) = Y$
137	134 135 136	3jca	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \land F (2) = Y) \to (F (0) = Z \land F (1) = X \land F (2) = Y)$
138	137	orcd	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \land F (2) = Y) \to ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))$
139	138	3mix3d	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \land F (2) = Y) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$
140	139	ex	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
141		eqeq2	$⊢ Z = F (0) \to (F (2) = Z \leftrightarrow F (2) = F (0))$
142	141	eqcoms	$⊢ F (0) = Z \to (F (2) = Z \leftrightarrow F (2) = F (0))$
143	142	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (2) = Z \leftrightarrow F (2) = F (0))$
144	97	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (2) = F (0) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
145	143 144	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
146	145	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
147	133 140 146	3jaod	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = X) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
148	147	ex	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (1) = X \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
149		simpllr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \land F (2) = X) \to F (0) = Z$
150		simplr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \land F (2) = X) \to F (1) = Y$
151		simpr	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \land F (2) = X) \to F (2) = X$
152	149 150 151	3jca	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \land F (2) = X) \to (F (0) = Z \land F (1) = Y \land F (2) = X)$
153	152	olcd	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \land F (2) = X) \to ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))$
154	153	3mix3d	$⊢ (((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \land F (2) = X) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$
155	154	ex	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \to (F (2) = X \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
156	46	adantl	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \to (F (2) = Y \leftrightarrow F (2) = F (1))$
157	79	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
158	157	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \to (F (2) = F (1) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
159	156 158	sylbid	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \to (F (2) = Y \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
160	145	adantr	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \to (F (2) = Z \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
161	155 159 160	3jaod	$⊢ ((F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \land F (1) = Y) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
162	161	ex	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (1) = Y \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
163		eqeq2	$⊢ Z = F (0) \to (F (1) = Z \leftrightarrow F (1) = F (0))$
164	163	eqcoms	$⊢ F (0) = Z \to (F (1) = Z \leftrightarrow F (1) = F (0))$
165	164	adantl	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (1) = Z \leftrightarrow F (1) = F (0))$
166	30	adantr	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (1) = F (0) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
167	165 166	sylbid	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to (F (1) = Z \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
168	148 162 167	3jaod	$⊢ (F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \land F (0) = Z) \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))))$
169	168	ex	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (F (0) = Z \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))))$
170	86 129 169	3jaod	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to ((F (0) = X \lor F (0) = Y \lor F (0) = Z) \to ((F (1) = X \lor F (1) = Y \lor F (1) = Z) \to ((F (2) = X \lor F (2) = Y \lor F (2) = Z) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))))$
171	170	3impd	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (((F (0) = X \lor F (0) = Y \lor F (0) = Z) \land (F (1) = X \lor F (1) = Y \lor F (1) = Z) \land (F (2) = X \lor F (2) = Y \lor F (2) = Z)) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
172	22 171	syl5	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to ((F (0) \in \{X, Y, Z\} \land F (1) \in \{X, Y, Z\} \land F (2) \in \{X, Y, Z\}) \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X))))$
173	6 12 18 172	mp3and	$⊢ F : (0 ..^3) \underset{1-1}{⟶} \{X, Y, Z\} \to (((F (0) = X \land F (1) = Y \land F (2) = Z) \lor (F (0) = X \land F (1) = Z \land F (2) = Y)) \lor ((F (0) = Y \land F (1) = X \land F (2) = Z) \lor (F (0) = Y \land F (1) = Z \land F (2) = X)) \lor ((F (0) = Z \land F (1) = X \land F (2) = Y) \lor (F (0) = Z \land F (1) = Y \land F (2) = X)))$

Metamath Proof Explorer

Theorem fvf1tp

Proof