Metamath Proof Explorer

Theorem grtri

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

Ref Expression
Hypotheses grtri.v ⊢ V = Vtx ⁡ G
grtri.e ⊢ E = Edg ⁡ G
Assertion grtri Could not format assertion : No typesetting found for |- ( G e. W -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) with typecode |-

Proof

Step Hyp Ref Expression
1 grtri.v ⊢ V = Vtx ⁡ G
2 grtri.e ⊢ E = Edg ⁡ G
3 df-grtri Could not format GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } ) : No typesetting found for |- GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } ) with typecode |-
4 3 a1i Could not format ( G e. W -> GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } ) ) : No typesetting found for |- ( G e. W -> GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } ) ) with typecode |-
5 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
6 5 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
7 fveq2 ⊢ g = G → Edg ⁡ g = Edg ⁡ G
8 7 2 eqtr4di ⊢ g = G → Edg ⁡ g = E
9 8 csbeq1d ⊢ g = G → ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e = ⦋ E / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
10 6 9 csbeq12dv ⊢ g = G → ⦋ Vtx ⁡ g / v⦌ ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e = ⦋ V / v⦌ ⦋ E / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
11 10 adantl ⊢ G ∈ W ∧ g = G → ⦋ Vtx ⁡ g / v⦌ ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e = ⦋ V / v⦌ ⦋ E / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
12 1 fvexi ⊢ V ∈ V
13 2 fvexi ⊢ E ∈ V
14 pweq ⊢ v = V → 𝒫 v = 𝒫 V
15 14 adantr ⊢ v = V ∧ e = E → 𝒫 v = 𝒫 V
16 eleq2 ⊢ e = E → f ⁡ 0 f ⁡ 1 ∈ e ↔ f ⁡ 0 f ⁡ 1 ∈ E
17 eleq2 ⊢ e = E → f ⁡ 0 f ⁡ 2 ∈ e ↔ f ⁡ 0 f ⁡ 2 ∈ E
18 eleq2 ⊢ e = E → f ⁡ 1 f ⁡ 2 ∈ e ↔ f ⁡ 1 f ⁡ 2 ∈ E
19 16 17 18 3anbi123d ⊢ e = E → f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e ↔ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
20 19 anbi2d ⊢ e = E → f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e ↔ f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
21 20 exbidv ⊢ e = E → ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e ↔ ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
22 21 adantl ⊢ v = V ∧ e = E → ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e ↔ ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
23 15 22 rabeqbidv ⊢ v = V ∧ e = E → t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e = t ∈ 𝒫 V | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
24 12 13 23 csbie2 ⊢ ⦋ V / v⦌ ⦋ E / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e = t ∈ 𝒫 V | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
25 11 24 eqtrdi ⊢ G ∈ W ∧ g = G → ⦋ Vtx ⁡ g / v⦌ ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e = t ∈ 𝒫 V | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E
26 elex ⊢ G ∈ W → G ∈ V
27 1 pweqi ⊢ 𝒫 V = 𝒫 Vtx ⁡ G
28 fvex ⊢ Vtx ⁡ G ∈ V
29 28 pwex ⊢ 𝒫 Vtx ⁡ G ∈ V
30 27 29 eqeltri ⊢ 𝒫 V ∈ V
31 30 rabex ⊢ t ∈ 𝒫 V | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ∈ V
32 31 a1i ⊢ G ∈ W → t ∈ 𝒫 V | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ E ∧ f ⁡ 0 f ⁡ 2 ∈ E ∧ f ⁡ 1 f ⁡ 2 ∈ E ∈ V
33 4 25 26 32 fvmptd Could not format ( G e. W -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) : No typesetting found for |- ( G e. W -> ( GrTriangles ` G ) = { t e. ~P V | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. E /\ { ( f ` 0 ) , ( f ` 2 ) } e. E /\ { ( f ` 1 ) , ( f ` 2 ) } e. E ) ) } ) with typecode |-