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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion grtrissvtx ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → 𝑇 ⊆ 𝑉 )

Proof

Step Hyp Ref Expression
1 grtrissvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 grtriprop ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) )
4 tpssi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → { 𝑥 , 𝑦 , 𝑧 } ⊆ 𝑉 )
5 4 3expa ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑉 ) → { 𝑥 , 𝑦 , 𝑧 } ⊆ 𝑉 )
6 sseq1 ⊢ ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } → ( 𝑇 ⊆ 𝑉 ↔ { 𝑥 , 𝑦 , 𝑧 } ⊆ 𝑉 ) )
7 6 3ad2ant1 ⊢ ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑇 ⊆ 𝑉 ↔ { 𝑥 , 𝑦 , 𝑧 } ⊆ 𝑉 ) )
8 5 7 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝑇 ⊆ 𝑉 ) )
9 8 rexlimdva ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝑇 ⊆ 𝑉 ) )
10 9 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑇 = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐺 ) ) ) → 𝑇 ⊆ 𝑉 )
11 3 10 syl ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → 𝑇 ⊆ 𝑉 )