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 ‘ 𝐺 ) → 𝑇 ⊆ 𝑉 )