Metamath Proof Explorer

Theorem grtri

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

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

Proof

Step Hyp Ref Expression
1 grtri.v 
 |-  V = ( Vtx ` G )
2 grtri.e 
 |-  E = ( Edg ` G )
3 df-grtri 
 |-  GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / 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 ) ) } )
4 3 a1i 
 |-  ( G e. W -> GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / 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 ) ) } ) )
5 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
6 5 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
7 fveq2 
 |-  ( g = G -> ( Edg ` g ) = ( Edg ` G ) )
8 7 2 eqtr4di 
 |-  ( g = G -> ( Edg ` g ) = E )
9 8 csbeq1d 
 |-  ( g = G -> [_ ( Edg ` g ) / 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 ) ) } = [_ 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 ) ) } )
10 6 9 csbeq12dv 
 |-  ( g = G -> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / 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 ) ) } = [_ V / v ]_ [_ 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 10 adantl 
 |-  ( ( G e. W /\ g = G ) -> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / 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 ) ) } = [_ V / v ]_ [_ 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 ) ) } )
12 1 fvexi 
 |-  V e. _V
13 2 fvexi 
 |-  E e. _V
14 pweq 
 |-  ( v = V -> ~P v = ~P V )
15 14 adantr 
 |-  ( ( v = V /\ e = E ) -> ~P v = ~P V )
16 eleq2 
 |-  ( e = E -> ( { ( f ` 0 ) , ( f ` 1 ) } e. e <-> { ( f ` 0 ) , ( f ` 1 ) } e. E ) )
17 eleq2 
 |-  ( e = E -> ( { ( f ` 0 ) , ( f ` 2 ) } e. e <-> { ( f ` 0 ) , ( f ` 2 ) } e. E ) )
18 eleq2 
 |-  ( e = E -> ( { ( f ` 1 ) , ( f ` 2 ) } e. e <-> { ( f ` 1 ) , ( f ` 2 ) } e. E ) )
19 16 17 18 3anbi123d 
 |-  ( e = E -> ( ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) <-> ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) )
20 19 anbi2d 
 |-  ( 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 ) ) <-> ( 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 ) ) ) )
21 20 exbidv 
 |-  ( 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 ) ) <-> 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 ) ) ) )
22 21 adantl 
 |-  ( ( v = V /\ 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 ) ) <-> 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 ) ) ) )
23 15 22 rabeqbidv 
 |-  ( ( v = V /\ 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 ) ) } = { 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 ) ) } )
24 12 13 23 csbie2 
 |-  [_ V / v ]_ [_ 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 ) ) } = { 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 ) ) }
25 11 24 eqtrdi 
 |-  ( ( G e. W /\ g = G ) -> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / 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 ) ) } )
26 elex 
 |-  ( G e. W -> G e. _V )
27 1 pweqi 
 |-  ~P V = ~P ( Vtx ` G )
28 fvex 
 |-  ( Vtx ` G ) e. _V
29 28 pwex 
 |-  ~P ( Vtx ` G ) e. _V
30 27 29 eqeltri 
 |-  ~P V e. _V
31 30 rabex 
 |-  { 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. _V
32 31 a1i 
 |-  ( G e. W -> { 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. _V )
33 4 25 26 32 fvmptd 
 |-  ( G e. W -> ( 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 ) ) } )