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

Metamath Proof Explorer

Theorem grtrissvtx

Description: A triangle is a subset of the vertices (of a graph). (Contributed by AV, 26-Jul-2025)

Ref Expression
Hypothesis grtrissvtx.v 
|- V = ( Vtx ` G )
Assertion grtrissvtx 
|- ( T e. ( GrTriangles ` G ) -> T C_ V )

Proof

Step Hyp Ref Expression
1 grtrissvtx.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( 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. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) )
4 tpssi 
 |-  ( ( x e. V /\ y e. V /\ z e. V ) -> { x , y , z } C_ V )
5 4 3expa 
 |-  ( ( ( x e. V /\ y e. V ) /\ z e. V ) -> { x , y , z } C_ V )
6 sseq1 
 |-  ( T = { x , y , z } -> ( T C_ V <-> { x , y , z } C_ V ) )
7 6 3ad2ant1 
 |-  ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) -> ( T C_ V <-> { x , y , z } C_ V ) )
8 5 7 syl5ibrcom 
 |-  ( ( ( x e. V /\ y e. V ) /\ z e. V ) -> ( ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) -> T C_ V ) )
9 8 rexlimdva 
 |-  ( ( x e. V /\ y e. V ) -> ( E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) -> T C_ V ) )
10 9 rexlimivv 
 |-  ( E. x e. V E. y e. V E. z e. V ( T = { x , y , z } /\ ( # ` T ) = 3 /\ ( { x , y } e. ( Edg ` G ) /\ { x , z } e. ( Edg ` G ) /\ { y , z } e. ( Edg ` G ) ) ) -> T C_ V )
11 3 10 syl 
 |-  ( T e. ( GrTriangles ` G ) -> T C_ V )