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=\mathrm{Vtx}\left(G\right)$$
Assertion	grtrissvtx	Could not format assertion : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> T C_ V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		grtrissvtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
3	1 2	grtriprop	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
4		tpssi	$$⊢\left(x\in V\wedge y\in V\wedge z\in V\right)\to \left\{x,y,z\right\}\subseteq V$$
5	4	3expa	$$⊢\left(\left(x\in V\wedge y\in V\right)\wedge z\in V\right)\to \left\{x,y,z\right\}\subseteq V$$
6		sseq1	$$⊢T=\left\{x,y,z\right\}\to \left(T\subseteq V\leftrightarrow \left\{x,y,z\right\}\subseteq V\right)$$
7	6	3ad2ant1	$$⊢\left(T=\left\{x,y,z\right\}\wedge \left|T\right|=3\wedge \left(\left\{x,y\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{x,z\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{y,z\right\}\in \mathrm{Edg}\left(G\right)\right)\right)\to \left(T\subseteq V\leftrightarrow \left\{x,y,z\right\}\subseteq V\right)$$
8	5 7	syl5ibrcom	$$⊢\left(\left(x\in V\wedge y\in V\right)\wedge z\in V\right)\to \left(\left(T=\left\{x,y,z\right\}\wedge \left|T\right|=3\wedge \left(\left\{x,y\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{x,z\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{y,z\right\}\in \mathrm{Edg}\left(G\right)\right)\right)\to T\subseteq V\right)$$
9	8	rexlimdva	$$⊢\left(x\in V\wedge y\in V\right)\to \left(\exists z\in V\left(T=\left\{x,y,z\right\}\wedge \left|T\right|=3\wedge \left(\left\{x,y\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{x,z\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{y,z\right\}\in \mathrm{Edg}\left(G\right)\right)\right)\to T\subseteq V\right)$$
10	9	rexlimivv	$$⊢\exists x\in V\exists y\in V\exists z\in V\left(T=\left\{x,y,z\right\}\wedge \left|T\right|=3\wedge \left(\left\{x,y\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{x,z\right\}\in \mathrm{Edg}\left(G\right)\wedge \left\{y,z\right\}\in \mathrm{Edg}\left(G\right)\right)\right)\to T\subseteq V$$
11	3 10	syl	Could not format ( T e. ( GrTriangles ` G ) -> T C_ V ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> T C_ V ) with typecode |-