Metamath Proof Explorer

Theorem incistruhgr

Description: Anincidence structure <. P , L , I >. "where P is a set whose elements are calledpoints, L is a distinct set whose elements are calledlines and I C_ ( P X. L ) is theincidence relation" (see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure ) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With P = ( BaseS ) and by defining two new slots for lines and incidence relations (analogous to LineG and Itv ) and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incidence structureis an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020)

Ref Expression
Hypotheses incistruhgr.v ⊢V=Vtx⁡G
incistruhgr.e ⊢E=iEdg⁡G
Assertion incistruhgr ⊢G∈W∧I⊆P×L∧ran⁡I=L→V=P∧E=e∈L⟼v∈P|vIe→G∈UHGraph

Proof

Step Hyp Ref Expression
1 incistruhgr.v ⊢V=Vtx⁡G
2 incistruhgr.e ⊢E=iEdg⁡G
3 rabeq ⊢V=P→v∈V|vIe=v∈P|vIe
4 3 mpteq2dv ⊢V=P→e∈L⟼v∈V|vIe=e∈L⟼v∈P|vIe
5 4 eqeq2d ⊢V=P→E=e∈L⟼v∈V|vIe↔E=e∈L⟼v∈P|vIe
6 xpeq1 ⊢V=P→V×L=P×L
7 6 sseq2d ⊢V=P→I⊆V×L↔I⊆P×L
8 7 3anbi2d ⊢V=P→G∈W∧I⊆V×L∧ran⁡I=L↔G∈W∧I⊆P×L∧ran⁡I=L
9 5 8 anbi12d ⊢V=P→E=e∈L⟼v∈V|vIe∧G∈W∧I⊆V×L∧ran⁡I=L↔E=e∈L⟼v∈P|vIe∧G∈W∧I⊆P×L∧ran⁡I=L
10 dmeq ⊢E=e∈L⟼v∈V|vIe→dom⁡E=dom⁡e∈L⟼v∈V|vIe
11 1 fvexi ⊢V∈V
12 11 rabex ⊢v∈V|vIe∈V
13 eqid ⊢e∈L⟼v∈V|vIe=e∈L⟼v∈V|vIe
14 12 13 dmmpti ⊢dom⁡e∈L⟼v∈V|vIe=L
15 10 14 eqtrdi ⊢E=e∈L⟼v∈V|vIe→dom⁡E=L
16 ssrab2 ⊢v∈V|vIe⊆V
17 16 a1i ⊢G∈W∧I⊆V×L∧ran⁡I=L∧e∈L→v∈V|vIe⊆V
18 12 elpw ⊢v∈V|vIe∈𝒫V↔v∈V|vIe⊆V
19 17 18 sylibr ⊢G∈W∧I⊆V×L∧ran⁡I=L∧e∈L→v∈V|vIe∈𝒫V
20 eleq2 ⊢ran⁡I=L→e∈ran⁡I↔e∈L
21 20 3ad2ant3 ⊢G∈W∧I⊆V×L∧ran⁡I=L→e∈ran⁡I↔e∈L
22 ssrelrn ⊢I⊆V×L∧e∈ran⁡I→∃v∈VvIe
23 22 ex ⊢I⊆V×L→e∈ran⁡I→∃v∈VvIe
24 23 3ad2ant2 ⊢G∈W∧I⊆V×L∧ran⁡I=L→e∈ran⁡I→∃v∈VvIe
25 21 24 sylbird ⊢G∈W∧I⊆V×L∧ran⁡I=L→e∈L→∃v∈VvIe
26 25 imp ⊢G∈W∧I⊆V×L∧ran⁡I=L∧e∈L→∃v∈VvIe
27 df-ne ⊢v∈V|vIe≠∅↔¬v∈V|vIe=∅
28 rabn0 ⊢v∈V|vIe≠∅↔∃v∈VvIe
29 27 28 bitr3i ⊢¬v∈V|vIe=∅↔∃v∈VvIe
30 26 29 sylibr ⊢G∈W∧I⊆V×L∧ran⁡I=L∧e∈L→¬v∈V|vIe=∅
31 12 elsn ⊢v∈V|vIe∈∅↔v∈V|vIe=∅
32 30 31 sylnibr ⊢G∈W∧I⊆V×L∧ran⁡I=L∧e∈L→¬v∈V|vIe∈∅
33 19 32 eldifd ⊢G∈W∧I⊆V×L∧ran⁡I=L∧e∈L→v∈V|vIe∈𝒫V∖∅
34 33 fmpttd ⊢G∈W∧I⊆V×L∧ran⁡I=L→e∈L⟼v∈V|vIe:L⟶𝒫V∖∅
35 simpl ⊢E=e∈L⟼v∈V|vIe∧dom⁡E=L→E=e∈L⟼v∈V|vIe
36 simpr ⊢E=e∈L⟼v∈V|vIe∧dom⁡E=L→dom⁡E=L
37 35 36 feq12d ⊢E=e∈L⟼v∈V|vIe∧dom⁡E=L→E:dom⁡E⟶𝒫V∖∅↔e∈L⟼v∈V|vIe:L⟶𝒫V∖∅
38 34 37 imbitrrid ⊢E=e∈L⟼v∈V|vIe∧dom⁡E=L→G∈W∧I⊆V×L∧ran⁡I=L→E:dom⁡E⟶𝒫V∖∅
39 15 38 mpdan ⊢E=e∈L⟼v∈V|vIe→G∈W∧I⊆V×L∧ran⁡I=L→E:dom⁡E⟶𝒫V∖∅
40 39 imp ⊢E=e∈L⟼v∈V|vIe∧G∈W∧I⊆V×L∧ran⁡I=L→E:dom⁡E⟶𝒫V∖∅
41 9 40 syl6bir ⊢V=P→E=e∈L⟼v∈P|vIe∧G∈W∧I⊆P×L∧ran⁡I=L→E:dom⁡E⟶𝒫V∖∅
42 41 expdimp ⊢V=P∧E=e∈L⟼v∈P|vIe→G∈W∧I⊆P×L∧ran⁡I=L→E:dom⁡E⟶𝒫V∖∅
43 42 impcom ⊢G∈W∧I⊆P×L∧ran⁡I=L∧V=P∧E=e∈L⟼v∈P|vIe→E:dom⁡E⟶𝒫V∖∅
44 1 2 isuhgr ⊢G∈W→G∈UHGraph↔E:dom⁡E⟶𝒫V∖∅
45 44 3ad2ant1 ⊢G∈W∧I⊆P×L∧ran⁡I=L→G∈UHGraph↔E:dom⁡E⟶𝒫V∖∅
46 45 adantr ⊢G∈W∧I⊆P×L∧ran⁡I=L∧V=P∧E=e∈L⟼v∈P|vIe→G∈UHGraph↔E:dom⁡E⟶𝒫V∖∅
47 43 46 mpbird ⊢G∈W∧I⊆P×L∧ran⁡I=L∧V=P∧E=e∈L⟼v∈P|vIe→G∈UHGraph
48 47 ex ⊢G∈W∧I⊆P×L∧ran⁡I=L→V=P∧E=e∈L⟼v∈P|vIe→G∈UHGraph