Metamath Proof Explorer

Theorem isgrtri

Description: A triangle in a graph. (Contributed by AV, 20-Jul-2025)

Ref Expression
Hypotheses grtri.v 
|- V = ( Vtx ` G )
grtri.e 
|- E = ( Edg ` G )
Assertion isgrtri 
|- ( 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 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 df-tp 
 |-  { x , y , z } = ( { x , y } u. { z } )
5 prelpwi 
 |-  ( ( x e. V /\ y e. V ) -> { x , y } e. ~P V )
6 snelpwi 
 |-  ( z e. V -> { z } e. ~P V )
7 5 6 anim12i 
 |-  ( ( ( x e. V /\ y e. V ) /\ z e. V ) -> ( { x , y } e. ~P V /\ { z } e. ~P V ) )
8 7 anasss 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( { x , y } e. ~P V /\ { z } e. ~P V ) )
9 pwuncl 
 |-  ( ( { x , y } e. ~P V /\ { z } e. ~P V ) -> ( { x , y } u. { z } ) e. ~P V )
10 8 9 syl 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( { x , y } u. { z } ) e. ~P V )
11 4 10 eqeltrid 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { x , y , z } e. ~P V )
12 11 adantr 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> { x , y , z } e. ~P V )
13 eleq1 
 |-  ( T = { x , y , z } -> ( T e. ~P V <-> { x , y , z } e. ~P V ) )
14 13 3ad2ant1 
 |-  ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( T e. ~P V <-> { x , y , z } e. ~P V ) )
15 14 adantl 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( T e. ~P V <-> { x , y , z } e. ~P V ) )
16 12 15 mpbird 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> T e. ~P V )
17 ovex 
 |-  ( 0 ..^ 3 ) e. _V
18 17 mptex 
 |-  ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) e. _V
19 18 a1i 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) e. _V )
20 3anass 
 |-  ( ( x e. V /\ y e. V /\ z e. V ) <-> ( x e. V /\ ( y e. V /\ z e. V ) ) )
21 20 biimpri 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( x e. V /\ y e. V /\ z e. V ) )
22 fveq2 
 |-  ( T = { x , y , z } -> ( # ` T ) = ( # ` { x , y , z } ) )
23 22 eqcomd 
 |-  ( T = { x , y , z } -> ( # ` { x , y , z } ) = ( # ` T ) )
24 23 3ad2ant1 
 |-  ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( # ` { x , y , z } ) = ( # ` T ) )
25 simp2 
 |-  ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( # ` T ) = 3 )
26 24 25 eqtrd 
 |-  ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( # ` { x , y , z } ) = 3 )
27 eqid 
 |-  ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) )
28 eqid 
 |-  { x , y , z } = { x , y , z }
29 27 28 tpf1o 
 |-  ( ( ( x e. V /\ y e. V /\ z e. V ) /\ ( # ` { x , y , z } ) = 3 ) -> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } )
30 21 26 29 syl2an 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } )
31 f1oeq3 
 |-  ( T = { x , y , z } -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T <-> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } ) )
32 31 3ad2ant1 
 |-  ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T <-> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } ) )
33 32 adantl 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T <-> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> { x , y , z } ) )
34 30 33 mpbird 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T )
35 27 tpf1ofv0 
 |-  ( x e. V -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) = x )
36 35 adantr 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) = x )
37 27 tpf1ofv1 
 |-  ( y e. V -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) = y )
38 37 adantr 
 |-  ( ( y e. V /\ z e. V ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) = y )
39 38 adantl 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) = y )
40 36 39 preq12d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } = { x , y } )
41 40 eqcomd 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { x , y } = { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } )
42 41 eleq1d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( { x , y } e. E <-> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E ) )
43 27 tpf1ofv2 
 |-  ( z e. V -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) = z )
44 43 adantl 
 |-  ( ( y e. V /\ z e. V ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) = z )
45 44 adantl 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) = z )
46 36 45 preq12d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } = { x , z } )
47 46 eqcomd 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { x , z } = { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } )
48 47 eleq1d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( { x , z } e. E <-> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) )
49 39 45 preq12d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } = { y , z } )
50 49 eqcomd 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> { y , z } = { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } )
51 50 eleq1d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( { y , z } e. E <-> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) )
52 42 48 51 3anbi123d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) <-> ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) ) )
53 52 biimpd 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) ) )
54 53 2a1d 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( T = { x , y , z } -> ( ( # ` T ) = 3 -> ( ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) -> ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) ) ) ) )
55 54 3imp2 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) )
56 34 55 jca 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) ) )
57 f1oeq1 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( f : ( 0 ..^ 3 ) -1-1-onto-> T <-> ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T ) )
58 fveq1 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( f ` 0 ) = ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) )
59 fveq1 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( f ` 1 ) = ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) )
60 58 59 preq12d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> { ( f ` 0 ) , ( f ` 1 ) } = { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } )
61 60 eleq1d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( { ( f ` 0 ) , ( f ` 1 ) } e. E <-> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E ) )
62 fveq1 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( f ` 2 ) = ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) )
63 58 62 preq12d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> { ( f ` 0 ) , ( f ` 2 ) } = { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } )
64 63 eleq1d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( { ( f ` 0 ) , ( f ` 2 ) } e. E <-> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) )
65 59 62 preq12d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> { ( f ` 1 ) , ( f ` 2 ) } = { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } )
66 65 eleq1d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( { ( f ` 1 ) , ( f ` 2 ) } e. E <-> { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) )
67 61 64 66 3anbi123d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) <-> ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) ) )
68 57 67 anbi12d 
 |-  ( f = ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) -> ( ( 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 ) ) <-> ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) : ( 0 ..^ 3 ) -1-1-onto-> T /\ ( { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 0 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E /\ { ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 1 ) , ( ( i e. ( 0 ..^ 3 ) |-> if ( i = 0 , x , if ( i = 1 , y , z ) ) ) ` 2 ) } e. E ) ) ) )
69 19 56 68 spcedv 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } 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 ) ) )
70 16 69 jca 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } 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 ) ) ) )
71 1 1vgrex 
 |-  ( x e. V -> G e. _V )
72 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 ) ) } )
73 72 eleq2d 
 |-  ( G e. _V -> ( 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 ) ) } ) )
74 71 73 syl 
 |-  ( x e. V -> ( 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 ) ) } ) )
75 f1oeq3 
 |-  ( t = T -> ( f : ( 0 ..^ 3 ) -1-1-onto-> t <-> f : ( 0 ..^ 3 ) -1-1-onto-> T ) )
76 75 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 ) ) ) )
77 76 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 ) ) ) )
78 77 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 ) ) ) )
79 74 78 bitrdi 
 |-  ( x e. V -> ( 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 ) ) ) ) )
80 79 adantr 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( 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 ) ) ) ) )
81 80 adantr 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> ( 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 ) ) ) ) )
82 70 81 mpbird 
 |-  ( ( ( x e. V /\ ( y e. V /\ z e. V ) ) /\ ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) ) -> T e. ( GrTriangles ` G ) )
83 82 ex 
 |-  ( ( x e. V /\ ( y e. V /\ z e. V ) ) -> ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. E /\ { x , z } e. E /\ { y , z } e. E ) ) -> T e. ( GrTriangles ` G ) ) )
84 83 rexlimdvva 
 |-  ( 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 ) ) -> T e. ( GrTriangles ` G ) ) )
85 84 rexlimiv 
 |-  ( 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 ) ) -> T e. ( GrTriangles ` G ) )
86 3 85 impbii 
 |-  ( 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 ) ) )