This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grtriprop

Description: The properties of a triangle. (Contributed by AV, 25-Jul-2025)

Ref Expression
Hypotheses grtri.v 
|- V = ( Vtx ` G )
grtri.e 
|- E = ( Edg ` G )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 grtri.v 
 |-  V = ( Vtx ` G )
2 grtri.e 
 |-  E = ( Edg ` G )
3 elfvex 
 |-  ( T e. ( GrTriangles ` G ) -> G e. _V )
4 1 2 grtri 
 |-  ( G e. _V -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( 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 ) ) } )
5 3 4 syl 
 |-  ( T e. ( GrTriangles ` G ) -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( 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 ) ) } )
6 5 eleq2d 
 |-  ( T e. ( GrTriangles ` G ) -> ( T e. ( GrTriangles ` G ) <-> T e. { t e. ~P V | E. f ( 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 ) ) } ) )
7 f1oeq3 
 |-  ( t = T -> ( f : ( 0 ..^ 3 ) -1-1-onto-> t <-> f : ( 0 ..^ 3 ) -1-1-onto-> T ) )
8 7 anbi1d 
 |-  ( t = T -> ( ( 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 ) ) <-> ( 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 ) ) ) )
9 8 exbidv 
 |-  ( t = T -> ( E. f ( 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 ) ) <-> E. f ( 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 ) ) ) )
10 9 elrab 
 |-  ( T e. { t e. ~P V | E. f ( 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 ) ) } <-> ( T e. ~P V /\ E. f ( 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 ) ) ) )
11 6 10 bitrdi 
 |-  ( T e. ( GrTriangles ` G ) -> ( T e. ( GrTriangles ` G ) <-> ( T e. ~P V /\ E. f ( 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 ) ) ) ) )
12 ovexd 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( 0 ..^ 3 ) e. _V )
13 simpr 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> f : ( 0 ..^ 3 ) -1-1-onto-> T )
14 12 13 hasheqf1od 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) )
15 eqcom 
 |-  ( ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) <-> ( # ` T ) = ( # ` ( 0 ..^ 3 ) ) )
16 3nn0 
 |-  3 e. NN0
17 hashfzo0 
 |-  ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
18 16 17 mp1i 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( # ` ( 0 ..^ 3 ) ) = 3 )
19 18 eqeq2d 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( ( # ` T ) = ( # ` ( 0 ..^ 3 ) ) <-> ( # ` T ) = 3 ) )
20 15 19 bitrid 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) <-> ( # ` T ) = 3 ) )
21 hash3tpb 
 |-  ( T e. ~P V -> ( ( # ` T ) = 3 <-> E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
22 21 adantr 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( ( # ` T ) = 3 <-> E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
23 22 biimpa 
 |-  ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) -> E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) )
24 elpwi 
 |-  ( T e. ~P V -> T C_ V )
25 ss2rexv 
 |-  ( T C_ V -> ( E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. x e. V E. y e. V E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
26 ssrexv 
 |-  ( T C_ V -> ( E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
27 26 reximdv 
 |-  ( T C_ V -> ( E. y e. V E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
28 27 reximdv 
 |-  ( T C_ V -> ( E. x e. V E. y e. V E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
29 25 28 syld 
 |-  ( T C_ V -> ( E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
30 24 29 syl 
 |-  ( T e. ~P V -> ( E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
31 30 adantr 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
32 31 adantr 
 |-  ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) -> ( E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) )
33 simprr 
 |-  ( ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) /\ ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) -> T = { x , y , z } )
34 simp-5r 
 |-  ( ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) /\ ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) -> ( # ` T ) = 3 )
35 f1oeq3 
 |-  ( T = { x , y , z } -> ( f : ( 0 ..^ 3 ) -1-1-onto-> T <-> f : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } ) )
36 grtriproplem 
 |-  ( ( 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 ) ) -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) )
37 36 2a1d 
 |-  ( ( 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 ) ) -> ( ( x e. V /\ y e. V ) -> ( z e. V -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) )
38 37 ex 
 |-  ( 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 ) -> ( ( x e. V /\ y e. V ) -> ( z e. V -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) ) )
39 38 a1d 
 |-  ( f : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } -> ( ( # ` T ) = 3 -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> ( ( x e. V /\ y e. V ) -> ( z e. V -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) ) ) )
40 35 39 biimtrdi 
 |-  ( T = { x , y , z } -> ( f : ( 0 ..^ 3 ) -1-1-onto-> T -> ( ( # ` T ) = 3 -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> ( ( x e. V /\ y e. V ) -> ( z e. V -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) ) ) ) )
41 40 adantld 
 |-  ( T = { x , y , z } -> ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( ( # ` T ) = 3 -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> ( ( x e. V /\ y e. V ) -> ( z e. V -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) ) ) ) )
42 41 imp4c 
 |-  ( T = { x , y , z } -> ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) -> ( ( x e. V /\ y e. V ) -> ( z e. V -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) ) )
43 42 imp4c 
 |-  ( T = { x , y , z } -> ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) )
44 43 adantl 
 |-  ( ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) )
45 44 impcom 
 |-  ( ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) /\ ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) -> ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) )
46 33 34 45 3jca 
 |-  ( ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) /\ ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) ) -> ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) )
47 46 ex 
 |-  ( ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) /\ z e. V ) -> ( ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) )
48 47 reximdva 
 |-  ( ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) /\ ( x e. V /\ y e. V ) ) -> ( E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) )
49 48 reximdvva 
 |-  ( ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) -> ( E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> 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 ) ) ) )
50 49 ex 
 |-  ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> ( E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> 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 ) ) ) ) )
51 50 com23 
 |-  ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) -> ( E. x e. V E. y e. V E. z e. V ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> 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 ) ) ) ) )
52 32 51 syld 
 |-  ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) -> ( E. x e. T E. y e. T E. z e. T ( ( x =/= y /\ x =/= z /\ y =/= z ) /\ T = { x , y , z } ) -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> 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 ) ) ) ) )
53 23 52 mpd 
 |-  ( ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) /\ ( # ` T ) = 3 ) -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> 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 ) ) ) )
54 53 ex 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( ( # ` T ) = 3 -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> 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 ) ) ) ) )
55 20 54 sylbid 
 |-  ( ( T e. ~P V /\ f : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) -> 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 ) ) ) ) )
56 14 55 mpd 
 |-  ( ( T e. ~P V /\ 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 ) -> 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 ) ) ) )
57 56 expimpd 
 |-  ( T e. ~P V -> ( ( 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 ) ) -> 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 ) ) ) )
58 57 exlimdv 
 |-  ( T e. ~P V -> ( E. f ( 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 ) ) -> 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 ) ) ) )
59 58 imp 
 |-  ( ( T e. ~P V /\ E. f ( 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 ) ) ) -> 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 ) ) )
60 11 59 biimtrdi 
 |-  ( T e. ( GrTriangles ` G ) -> ( 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 ) ) ) )
61 60 pm2.43i 
 |-  ( 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 ) ) )