grtriproplem

		Ref	Expression
	Assertion	grtriproplem	$⊢ (f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$

Proof

Step	Hyp	Ref	Expression
1		f1of1	$⊢ f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \to f : (0 ..^3) \underset{1-1}{⟶} \{x, y, z\}$
2		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)))$
3		simp1	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to f (0) = x$
4		simp2	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to f (1) = y$
5	3 4	preq12d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to \{f (0), f (1)\} = \{x, y\}$
6	5	eleq1d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to (\{f (0), f (1)\} \in E \leftrightarrow \{x, y\} \in E)$
7		simp3	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to f (2) = z$
8	3 7	preq12d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to \{f (0), f (2)\} = \{x, z\}$
9	8	eleq1d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to (\{f (0), f (2)\} \in E \leftrightarrow \{x, z\} \in E)$
10	4 7	preq12d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to \{f (1), f (2)\} = \{y, z\}$
11	10	eleq1d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to (\{f (1), f (2)\} \in E \leftrightarrow \{y, z\} \in E)$
12	6 9 11	3anbi123d	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \leftrightarrow (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
13	12	biimpd	$⊢ (f (0) = x \land f (1) = y \land f (2) = z) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
14		simp1	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to f (0) = x$
15		simp2	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to f (1) = z$
16	14 15	preq12d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to \{f (0), f (1)\} = \{x, z\}$
17	16	eleq1d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to (\{f (0), f (1)\} \in E \leftrightarrow \{x, z\} \in E)$
18		simp3	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to f (2) = y$
19	14 18	preq12d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to \{f (0), f (2)\} = \{x, y\}$
20	19	eleq1d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to (\{f (0), f (2)\} \in E \leftrightarrow \{x, y\} \in E)$
21	15 18	preq12d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to \{f (1), f (2)\} = \{z, y\}$
22	21	eleq1d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to (\{f (1), f (2)\} \in E \leftrightarrow \{z, y\} \in E)$
23	17 20 22	3anbi123d	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \leftrightarrow (\{x, z\} \in E \land \{x, y\} \in E \land \{z, y\} \in E))$
24		3ancoma	$⊢ (\{x, z\} \in E \land \{x, y\} \in E \land \{z, y\} \in E) \leftrightarrow (\{x, y\} \in E \land \{x, z\} \in E \land \{z, y\} \in E)$
25		prcom	$⊢ \{z, y\} = \{y, z\}$
26	25	eleq1i	$⊢ \{z, y\} \in E \leftrightarrow \{y, z\} \in E$
27	26	3anbi3i	$⊢ (\{x, y\} \in E \land \{x, z\} \in E \land \{z, y\} \in E) \leftrightarrow (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
28	24 27	sylbb	$⊢ (\{x, z\} \in E \land \{x, y\} \in E \land \{z, y\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
29	23 28	biimtrdi	$⊢ (f (0) = x \land f (1) = z \land f (2) = y) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
30	13 29	jaoi	$⊢ ((f (0) = x \land f (1) = y \land f (2) = z) \lor (f (0) = x \land f (1) = z \land f (2) = y)) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
31		simp1	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to f (0) = y$
32		simp2	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to f (1) = x$
33	31 32	preq12d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to \{f (0), f (1)\} = \{y, x\}$
34	33	eleq1d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to (\{f (0), f (1)\} \in E \leftrightarrow \{y, x\} \in E)$
35		simp3	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to f (2) = z$
36	31 35	preq12d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to \{f (0), f (2)\} = \{y, z\}$
37	36	eleq1d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to (\{f (0), f (2)\} \in E \leftrightarrow \{y, z\} \in E)$
38	32 35	preq12d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to \{f (1), f (2)\} = \{x, z\}$
39	38	eleq1d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to (\{f (1), f (2)\} \in E \leftrightarrow \{x, z\} \in E)$
40	34 37 39	3anbi123d	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \leftrightarrow (\{y, x\} \in E \land \{y, z\} \in E \land \{x, z\} \in E))$
41		3ancomb	$⊢ (\{y, x\} \in E \land \{y, z\} \in E \land \{x, z\} \in E) \leftrightarrow (\{y, x\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
42		prcom	$⊢ \{y, x\} = \{x, y\}$
43	42	eleq1i	$⊢ \{y, x\} \in E \leftrightarrow \{x, y\} \in E$
44	43	3anbi1i	$⊢ (\{y, x\} \in E \land \{x, z\} \in E \land \{y, z\} \in E) \leftrightarrow (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
45	41 44	sylbb	$⊢ (\{y, x\} \in E \land \{y, z\} \in E \land \{x, z\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
46	40 45	biimtrdi	$⊢ (f (0) = y \land f (1) = x \land f (2) = z) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
47		simp1	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to f (0) = y$
48		simp2	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to f (1) = z$
49	47 48	preq12d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to \{f (0), f (1)\} = \{y, z\}$
50	49	eleq1d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to (\{f (0), f (1)\} \in E \leftrightarrow \{y, z\} \in E)$
51		simp3	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to f (2) = x$
52	47 51	preq12d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to \{f (0), f (2)\} = \{y, x\}$
53	52	eleq1d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to (\{f (0), f (2)\} \in E \leftrightarrow \{y, x\} \in E)$
54	48 51	preq12d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to \{f (1), f (2)\} = \{z, x\}$
55	54	eleq1d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to (\{f (1), f (2)\} \in E \leftrightarrow \{z, x\} \in E)$
56	50 53 55	3anbi123d	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \leftrightarrow (\{y, z\} \in E \land \{y, x\} \in E \land \{z, x\} \in E))$
57		3anrot	$⊢ (\{y, z\} \in E \land \{y, x\} \in E \land \{z, x\} \in E) \leftrightarrow (\{y, x\} \in E \land \{z, x\} \in E \land \{y, z\} \in E)$
58		prcom	$⊢ \{z, x\} = \{x, z\}$
59	58	eleq1i	$⊢ \{z, x\} \in E \leftrightarrow \{x, z\} \in E$
60		biid	$⊢ \{y, z\} \in E \leftrightarrow \{y, z\} \in E$
61	43 59 60	3anbi123i	$⊢ (\{y, x\} \in E \land \{z, x\} \in E \land \{y, z\} \in E) \leftrightarrow (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
62	57 61	sylbb	$⊢ (\{y, z\} \in E \land \{y, x\} \in E \land \{z, x\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
63	56 62	biimtrdi	$⊢ (f (0) = y \land f (1) = z \land f (2) = x) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
64	46 63	jaoi	$⊢ ((f (0) = y \land f (1) = x \land f (2) = z) \lor (f (0) = y \land f (1) = z \land f (2) = x)) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
65		simp1	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to f (0) = z$
66		simp2	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to f (1) = x$
67	65 66	preq12d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to \{f (0), f (1)\} = \{z, x\}$
68	67	eleq1d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to (\{f (0), f (1)\} \in E \leftrightarrow \{z, x\} \in E)$
69		simp3	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to f (2) = y$
70	65 69	preq12d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to \{f (0), f (2)\} = \{z, y\}$
71	70	eleq1d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to (\{f (0), f (2)\} \in E \leftrightarrow \{z, y\} \in E)$
72	66 69	preq12d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to \{f (1), f (2)\} = \{x, y\}$
73	72	eleq1d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to (\{f (1), f (2)\} \in E \leftrightarrow \{x, y\} \in E)$
74	68 71 73	3anbi123d	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \leftrightarrow (\{z, x\} \in E \land \{z, y\} \in E \land \{x, y\} \in E))$
75		3anrot	$⊢ (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E) \leftrightarrow (\{x, z\} \in E \land \{y, z\} \in E \land \{x, y\} \in E)$
76		prcom	$⊢ \{x, z\} = \{z, x\}$
77	76	eleq1i	$⊢ \{x, z\} \in E \leftrightarrow \{z, x\} \in E$
78		prcom	$⊢ \{y, z\} = \{z, y\}$
79	78	eleq1i	$⊢ \{y, z\} \in E \leftrightarrow \{z, y\} \in E$
80		biid	$⊢ \{x, y\} \in E \leftrightarrow \{x, y\} \in E$
81	77 79 80	3anbi123i	$⊢ (\{x, z\} \in E \land \{y, z\} \in E \land \{x, y\} \in E) \leftrightarrow (\{z, x\} \in E \land \{z, y\} \in E \land \{x, y\} \in E)$
82	75 81	sylbbr	$⊢ (\{z, x\} \in E \land \{z, y\} \in E \land \{x, y\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
83	74 82	biimtrdi	$⊢ (f (0) = z \land f (1) = x \land f (2) = y) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
84		simp1	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to f (0) = z$
85		simp2	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to f (1) = y$
86	84 85	preq12d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to \{f (0), f (1)\} = \{z, y\}$
87	86	eleq1d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to (\{f (0), f (1)\} \in E \leftrightarrow \{z, y\} \in E)$
88		simp3	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to f (2) = x$
89	84 88	preq12d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to \{f (0), f (2)\} = \{z, x\}$
90	89	eleq1d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to (\{f (0), f (2)\} \in E \leftrightarrow \{z, x\} \in E)$
91	85 88	preq12d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to \{f (1), f (2)\} = \{y, x\}$
92	91	eleq1d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to (\{f (1), f (2)\} \in E \leftrightarrow \{y, x\} \in E)$
93	87 90 92	3anbi123d	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \leftrightarrow (\{z, y\} \in E \land \{z, x\} \in E \land \{y, x\} \in E))$
94		3anrev	$⊢ (\{z, y\} \in E \land \{z, x\} \in E \land \{y, x\} \in E) \leftrightarrow (\{y, x\} \in E \land \{z, x\} \in E \land \{z, y\} \in E)$
95	43 59 26	3anbi123i	$⊢ (\{y, x\} \in E \land \{z, x\} \in E \land \{z, y\} \in E) \leftrightarrow (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
96	94 95	sylbb	$⊢ (\{z, y\} \in E \land \{z, x\} \in E \land \{y, x\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$
97	93 96	biimtrdi	$⊢ (f (0) = z \land f (1) = y \land f (2) = x) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
98	83 97	jaoi	$⊢ ((f (0) = z \land f (1) = x \land f (2) = y) \lor (f (0) = z \land f (1) = y \land f (2) = x)) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
99	30 64 98	3jaoi	$⊢ (((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))) \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
100	1 2 99	3syl	$⊢ f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \to ((\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E))$
101	100	imp	$⊢ (f : (0 ..^3) \underset{1-1 onto}{⟶} \{x, y, z\} \land (\{f (0), f (1)\} \in E \land \{f (0), f (2)\} \in E \land \{f (1), f (2)\} \in E)) \to (\{x, y\} \in E \land \{x, z\} \in E \land \{y, z\} \in E)$

Metamath Proof Explorer

Theorem grtriproplem

Proof