grtrif1o

Description: Any bijection onto a triangle preserves the edges of the triangle. (Contributed by AV, 25-Jul-2025)

	Ref	Expression
Hypotheses	grtri.v	\|- V = ( Vtx ` G )
	grtri.e	\|- E = ( Edg ` G )
Assertion	grtrif1o	\|- ( ( T e. ( GrTriangles ` G ) /\ F : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) )

Proof

Step	Hyp	Ref	Expression
1		grtri.v	\|- V = ( Vtx ` G )
2		grtri.e	\|- E = ( Edg ` G )
3	1 2	grtriprop	\|- ( T e. ( GrTriangles ` G ) -> E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) )
4		f1oeq3	\|- ( T = { x , y , z } -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T <-> F : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } ) )
5	4	adantr	\|- ( ( T = { x , y , z } /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T <-> F : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } ) )
6		preq12	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y ) -> { ( F ` 0 ) , ( F ` 1 ) } = { x , y } )
7	6	eleq1d	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { x , y } e. E ) )
8	7	3adant3	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { x , y } e. E ) )
9		preq12	\|- ( ( ( F ` 0 ) = x /\ ( F ` 2 ) = z ) -> { ( F ` 0 ) , ( F ` 2 ) } = { x , z } )
10	9	eleq1d	\|- ( ( ( F ` 0 ) = x /\ ( F ` 2 ) = z ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { x , z } e. E ) )
11	10	3adant2	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { x , z } e. E ) )
12		preq12	\|- ( ( ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> { ( F ` 1 ) , ( F ` 2 ) } = { y , z } )
13	12	eleq1d	\|- ( ( ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { y , z } e. E ) )
14	13	3adant1	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { y , z } e. E ) )
15	8 11 14	3anbi123d	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> ( ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) <-> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) )
16	15	biimprd	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
17		3ancoma	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) <-> ( { x , z } e. E /\ { x , y } e. E /\ { y , z } e. E ) )
18		prcom	\|- { y , z } = { z , y }
19	18	eleq1i	\|- ( { y , z } e. E <-> { z , y } e. E )
20	19	3anbi3i	\|- ( ( { x , z } e. E /\ { x , y } e. E /\ { y , z } e. E ) <-> ( { x , z } e. E /\ { x , y } e. E /\ { z , y } e. E ) )
21	17 20	sylbb	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { x , z } e. E /\ { x , y } e. E /\ { z , y } e. E ) )
22		preq12	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z ) -> { ( F ` 0 ) , ( F ` 1 ) } = { x , z } )
23	22	eleq1d	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { x , z } e. E ) )
24	23	3adant3	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { x , z } e. E ) )
25		preq12	\|- ( ( ( F ` 0 ) = x /\ ( F ` 2 ) = y ) -> { ( F ` 0 ) , ( F ` 2 ) } = { x , y } )
26	25	eleq1d	\|- ( ( ( F ` 0 ) = x /\ ( F ` 2 ) = y ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { x , y } e. E ) )
27	26	3adant2	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { x , y } e. E ) )
28		preq12	\|- ( ( ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> { ( F ` 1 ) , ( F ` 2 ) } = { z , y } )
29	28	eleq1d	\|- ( ( ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { z , y } e. E ) )
30	29	3adant1	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { z , y } e. E ) )
31	24 27 30	3anbi123d	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> ( ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) <-> ( { x , z } e. E /\ { x , y } e. E /\ { z , y } e. E ) ) )
32	21 31	imbitrrid	\|- ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
33	16 32	jaoi	\|- ( ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
34		3ancomb	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) <-> ( { x , y } e. E /\ { y , z } e. E /\ { x , z } e. E ) )
35		prcom	\|- { x , y } = { y , x }
36	35	eleq1i	\|- ( { x , y } e. E <-> { y , x } e. E )
37	36	3anbi1i	\|- ( ( { x , y } e. E /\ { y , z } e. E /\ { x , z } e. E ) <-> ( { y , x } e. E /\ { y , z } e. E /\ { x , z } e. E ) )
38	34 37	sylbb	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { y , x } e. E /\ { y , z } e. E /\ { x , z } e. E ) )
39		preq12	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x ) -> { ( F ` 0 ) , ( F ` 1 ) } = { y , x } )
40	39	eleq1d	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { y , x } e. E ) )
41	40	3adant3	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { y , x } e. E ) )
42		preq12	\|- ( ( ( F ` 0 ) = y /\ ( F ` 2 ) = z ) -> { ( F ` 0 ) , ( F ` 2 ) } = { y , z } )
43	42	eleq1d	\|- ( ( ( F ` 0 ) = y /\ ( F ` 2 ) = z ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { y , z } e. E ) )
44	43	3adant2	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { y , z } e. E ) )
45		preq12	\|- ( ( ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> { ( F ` 1 ) , ( F ` 2 ) } = { x , z } )
46	45	eleq1d	\|- ( ( ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { x , z } e. E ) )
47	46	3adant1	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { x , z } e. E ) )
48	41 44 47	3anbi123d	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> ( ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) <-> ( { y , x } e. E /\ { y , z } e. E /\ { x , z } e. E ) ) )
49	38 48	imbitrrid	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
50		3anrot	\|- ( ( { y , z } e. E /\ { x , y } e. E /\ { x , z } e. E ) <-> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) )
51		biid	\|- ( { y , z } e. E <-> { y , z } e. E )
52		prcom	\|- { x , z } = { z , x }
53	52	eleq1i	\|- ( { x , z } e. E <-> { z , x } e. E )
54	51 36 53	3anbi123i	\|- ( ( { y , z } e. E /\ { x , y } e. E /\ { x , z } e. E ) <-> ( { y , z } e. E /\ { y , x } e. E /\ { z , x } e. E ) )
55	50 54	sylbb1	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { y , z } e. E /\ { y , x } e. E /\ { z , x } e. E ) )
56		preq12	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z ) -> { ( F ` 0 ) , ( F ` 1 ) } = { y , z } )
57	56	eleq1d	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { y , z } e. E ) )
58	57	3adant3	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { y , z } e. E ) )
59		preq12	\|- ( ( ( F ` 0 ) = y /\ ( F ` 2 ) = x ) -> { ( F ` 0 ) , ( F ` 2 ) } = { y , x } )
60	59	eleq1d	\|- ( ( ( F ` 0 ) = y /\ ( F ` 2 ) = x ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { y , x } e. E ) )
61	60	3adant2	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { y , x } e. E ) )
62		preq12	\|- ( ( ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> { ( F ` 1 ) , ( F ` 2 ) } = { z , x } )
63	62	eleq1d	\|- ( ( ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { z , x } e. E ) )
64	63	3adant1	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { z , x } e. E ) )
65	58 61 64	3anbi123d	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> ( ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) <-> ( { y , z } e. E /\ { y , x } e. E /\ { z , x } e. E ) ) )
66	55 65	imbitrrid	\|- ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
67	49 66	jaoi	\|- ( ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
68		3anrot	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) <-> ( { x , z } e. E /\ { y , z } e. E /\ { x , y } e. E ) )
69		biid	\|- ( { x , y } e. E <-> { x , y } e. E )
70	53 19 69	3anbi123i	\|- ( ( { x , z } e. E /\ { y , z } e. E /\ { x , y } e. E ) <-> ( { z , x } e. E /\ { z , y } e. E /\ { x , y } e. E ) )
71	68 70	sylbb	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { z , x } e. E /\ { z , y } e. E /\ { x , y } e. E ) )
72		preq12	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x ) -> { ( F ` 0 ) , ( F ` 1 ) } = { z , x } )
73	72	eleq1d	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { z , x } e. E ) )
74	73	3adant3	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { z , x } e. E ) )
75		preq12	\|- ( ( ( F ` 0 ) = z /\ ( F ` 2 ) = y ) -> { ( F ` 0 ) , ( F ` 2 ) } = { z , y } )
76	75	eleq1d	\|- ( ( ( F ` 0 ) = z /\ ( F ` 2 ) = y ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { z , y } e. E ) )
77	76	3adant2	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { z , y } e. E ) )
78		preq12	\|- ( ( ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> { ( F ` 1 ) , ( F ` 2 ) } = { x , y } )
79	78	eleq1d	\|- ( ( ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { x , y } e. E ) )
80	79	3adant1	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { x , y } e. E ) )
81	74 77 80	3anbi123d	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> ( ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) <-> ( { z , x } e. E /\ { z , y } e. E /\ { x , y } e. E ) ) )
82	71 81	imbitrrid	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
83		3anrev	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) <-> ( { y , z } e. E /\ { x , z } e. E /\ { x , y } e. E ) )
84	19 53 36	3anbi123i	\|- ( ( { y , z } e. E /\ { x , z } e. E /\ { x , y } e. E ) <-> ( { z , y } e. E /\ { z , x } e. E /\ { y , x } e. E ) )
85	83 84	sylbb	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { z , y } e. E /\ { z , x } e. E /\ { y , x } e. E ) )
86		preq12	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y ) -> { ( F ` 0 ) , ( F ` 1 ) } = { z , y } )
87	86	eleq1d	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { z , y } e. E ) )
88	87	3adant3	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E <-> { z , y } e. E ) )
89		preq12	\|- ( ( ( F ` 0 ) = z /\ ( F ` 2 ) = x ) -> { ( F ` 0 ) , ( F ` 2 ) } = { z , x } )
90	89	eleq1d	\|- ( ( ( F ` 0 ) = z /\ ( F ` 2 ) = x ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { z , x } e. E ) )
91	90	3adant2	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> ( { ( F ` 0 ) , ( F ` 2 ) } e. E <-> { z , x } e. E ) )
92		preq12	\|- ( ( ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> { ( F ` 1 ) , ( F ` 2 ) } = { y , x } )
93	92	eleq1d	\|- ( ( ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { y , x } e. E ) )
94	93	3adant1	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> ( { ( F ` 1 ) , ( F ` 2 ) } e. E <-> { y , x } e. E ) )
95	88 91 94	3anbi123d	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> ( ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) <-> ( { z , y } e. E /\ { z , x } e. E /\ { y , x } e. E ) ) )
96	85 95	imbitrrid	\|- ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
97	82 96	jaoi	\|- ( ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) \/ ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
98	33 67 97	3jaoi	\|- ( ( ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) ) \/ ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) ) \/ ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) \/ ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) ) ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
99		f1of1	\|- ( F : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } -> F : ( 0 ..^ 3 ) -1-1-> { x , y , z } )
100		fvf1tp	\|- ( F : ( 0 ..^ 3 ) -1-1-> { x , y , z } -> ( ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) ) \/ ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) ) \/ ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) \/ ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) ) ) )
101	99 100	syl	\|- ( F : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } -> ( ( ( ( F ` 0 ) = x /\ ( F ` 1 ) = y /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = x /\ ( F ` 1 ) = z /\ ( F ` 2 ) = y ) ) \/ ( ( ( F ` 0 ) = y /\ ( F ` 1 ) = x /\ ( F ` 2 ) = z ) \/ ( ( F ` 0 ) = y /\ ( F ` 1 ) = z /\ ( F ` 2 ) = x ) ) \/ ( ( ( F ` 0 ) = z /\ ( F ` 1 ) = x /\ ( F ` 2 ) = y ) \/ ( ( F ` 0 ) = z /\ ( F ` 1 ) = y /\ ( F ` 2 ) = x ) ) ) )
102	98 101	syl11	\|- ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
103	102	adantl	\|- ( ( T = { x , y , z } /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
104	5 103	sylbid	\|- ( ( T = { x , y , z } /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
105	104	3adant2	\|- ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
106	105	a1i	\|- ( ( y e. V /\ z e. V ) -> ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) ) )
107	106	rexlimivv	\|- ( E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
108	107	rexlimivw	\|- ( E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
109	3 108	syl	\|- ( T e. ( GrTriangles ` G ) -> ( F : ( 0 ..^ 3 ) -1-1-onto-> T -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) ) )
110	109	imp	\|- ( ( T e. ( GrTriangles ` G ) /\ F : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( F ` 0 ) , ( F ` 1 ) } e. E /\ { ( F ` 0 ) , ( F ` 2 ) } e. E /\ { ( F ` 1 ) , ( F ` 2 ) } e. E ) )

Metamath Proof Explorer

Theorem grtrif1o

Proof