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 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 = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
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 ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y z ⊆ V
5 4 3expa ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → x y z ⊆ V
6 sseq1 ⊢ T = x y z → T ⊆ V ↔ x y z ⊆ V
7 6 3ad2ant1 ⊢ T = x y z ∧ T = 3 ∧ x y ∈ Edg ⁡ G ∧ x z ∈ Edg ⁡ G ∧ y z ∈ Edg ⁡ G → T ⊆ V ↔ x y z ⊆ V
8 5 7 syl5ibrcom ⊢ x ∈ V ∧ y ∈ V ∧ z ∈ V → T = x y z ∧ T = 3 ∧ x y ∈ Edg ⁡ G ∧ x z ∈ Edg ⁡ G ∧ y z ∈ Edg ⁡ G → T ⊆ V
9 8 rexlimdva ⊢ x ∈ V ∧ y ∈ V → ∃ z ∈ V T = x y z ∧ T = 3 ∧ x y ∈ Edg ⁡ G ∧ x z ∈ Edg ⁡ G ∧ y z ∈ Edg ⁡ G → T ⊆ V
10 9 rexlimivv ⊢ ∃ x ∈ V ∃ y ∈ V ∃ z ∈ V T = x y z ∧ T = 3 ∧ x y ∈ Edg ⁡ G ∧ x z ∈ Edg ⁡ G ∧ y z ∈ Edg ⁡ G → T ⊆ 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 |-