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

Metamath Proof Explorer

Theorem grtri

Description: The triangles in a graph. (Contributed by AV, 20-Jul-2025)

Ref Expression
Hypotheses grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion grtri ( 𝐺 ∈ 𝑊 → ( GrTriangles ‘ 𝐺 ) = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grtri.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 df-grtri ⊢ GrTriangles = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } )
4 3 a1i ⊢ ( 𝐺 ∈ 𝑊 → GrTriangles = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } ) )
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
6 5 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
7 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
8 7 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = 𝐸 )
9 8 csbeq1d ⊢ ( 𝑔 = 𝐺 → ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } = ⦋ 𝐸 / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } )
10 6 9 csbeq12dv ⊢ ( 𝑔 = 𝐺 → ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } = ⦋ 𝑉 / 𝑣 ⦌ ⦋ 𝐸 / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } )
11 10 adantl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺 ) → ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } = ⦋ 𝑉 / 𝑣 ⦌ ⦋ 𝐸 / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } )
12 1 fvexi ⊢ 𝑉 ∈ V
13 2 fvexi ⊢ 𝐸 ∈ V
14 pweq ⊢ ( 𝑣 = 𝑉 → 𝒫 𝑣 = 𝒫 𝑉 )
15 14 adantr ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → 𝒫 𝑣 = 𝒫 𝑉 )
16 eleq2 ⊢ ( 𝑒 = 𝐸 → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ↔ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ) )
17 eleq2 ⊢ ( 𝑒 = 𝐸 → ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ↔ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) )
18 eleq2 ⊢ ( 𝑒 = 𝐸 → ( { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ↔ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) )
19 16 17 18 3anbi123d ⊢ ( 𝑒 = 𝐸 → ( ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ↔ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) )
20 19 anbi2d ⊢ ( 𝑒 = 𝐸 → ( ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) ↔ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
21 20 exbidv ⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
22 21 adantl ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) ) )
23 15 22 rabeqbidv ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )
24 12 13 23 csbie2 ⊢ ⦋ 𝑉 / 𝑣 ⦌ ⦋ 𝐸 / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) }
25 11 24 eqtrdi ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺 ) → ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )
26 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
27 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐺 )
28 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
29 28 pwex ⊢ 𝒫 ( Vtx ‘ 𝐺 ) ∈ V
30 27 29 eqeltri ⊢ 𝒫 𝑉 ∈ V
31 30 rabex ⊢ { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ∈ V
32 31 a1i ⊢ ( 𝐺 ∈ 𝑊 → { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } ∈ V )
33 4 25 26 32 fvmptd ⊢ ( 𝐺 ∈ 𝑊 → ( GrTriangles ‘ 𝐺 ) = { 𝑡 ∈ 𝒫 𝑉 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝐸 ) ) } )