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

Metamath Proof Explorer

Definition df-ushgr

Description: Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function e is an injective (one-to-one) function into subsets of the set of vertices v , representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of Bollobas p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of Diestel p. 27, where "E is a subset of [... the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020) (Revised by AV, 8-Oct-2020)

Ref Expression
Assertion df-ushgr USHGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ ( 𝒫 𝑣 ∖ { ∅ } ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cushgr ⊢ USHGraph
1 vg ⊢ 𝑔
2 cvtx ⊢ Vtx
3 1 cv ⊢ 𝑔
4 3 2 cfv ⊢ ( Vtx ‘ 𝑔 )
5 vv ⊢ 𝑣
6 ciedg ⊢ iEdg
7 3 6 cfv ⊢ ( iEdg ‘ 𝑔 )
8 ve ⊢ 𝑒
9 8 cv ⊢ 𝑒
10 9 cdm ⊢ dom 𝑒
11 5 cv ⊢ 𝑣
12 11 cpw ⊢ 𝒫 𝑣
13 c0 ⊢ ∅
14 13 csn ⊢ { ∅ }
15 12 14 cdif ⊢ ( 𝒫 𝑣 ∖ { ∅ } )
16 10 15 9 wf1 ⊢ 𝑒 : dom 𝑒 –1-1→ ( 𝒫 𝑣 ∖ { ∅ } )
17 16 8 7 wsbc ⊢ [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ ( 𝒫 𝑣 ∖ { ∅ } )
18 17 5 4 wsbc ⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ ( 𝒫 𝑣 ∖ { ∅ } )
19 18 1 cab ⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ ( 𝒫 𝑣 ∖ { ∅ } ) }
20 0 19 wceq ⊢ USHGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 –1-1→ ( 𝒫 𝑣 ∖ { ∅ } ) }