Metamath Proof Explorer

Theorem 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 ) )