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 | v I e → 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 | v I e = v ∈ P | v I e
4 3 mpteq2dv ⊢ V = P → e ∈ L ⟼ v ∈ V | v I e = e ∈ L ⟼ v ∈ P | v I e
5 4 eqeq2d ⊢ V = P → E = e ∈ L ⟼ v ∈ V | v I e ↔ E = e ∈ L ⟼ v ∈ P | v I e
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 | v I e ∧ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ↔ E = e ∈ L ⟼ v ∈ P | v I e ∧ G ∈ W ∧ I ⊆ P × L ∧ ran ⁡ I = L
10 dmeq ⊢ E = e ∈ L ⟼ v ∈ V | v I e → dom ⁡ E = dom ⁡ e ∈ L ⟼ v ∈ V | v I e
11 1 fvexi ⊢ V ∈ V
12 11 rabex ⊢ v ∈ V | v I e ∈ V
13 eqid ⊢ e ∈ L ⟼ v ∈ V | v I e = e ∈ L ⟼ v ∈ V | v I e
14 12 13 dmmpti ⊢ dom ⁡ e ∈ L ⟼ v ∈ V | v I e = L
15 10 14 eqtrdi ⊢ E = e ∈ L ⟼ v ∈ V | v I e → dom ⁡ E = L
16 ssrab2 ⊢ v ∈ V | v I e ⊆ V
17 16 a1i ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ∧ e ∈ L → v ∈ V | v I e ⊆ V
18 12 elpw ⊢ v ∈ V | v I e ∈ 𝒫 V ↔ v ∈ V | v I e ⊆ V
19 17 18 sylibr ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ∧ e ∈ L → v ∈ V | v I e ∈ 𝒫 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 ∈ V v I e
23 22 ex ⊢ I ⊆ V × L → e ∈ ran ⁡ I → ∃ v ∈ V v I e
24 23 3ad2ant2 ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L → e ∈ ran ⁡ I → ∃ v ∈ V v I e
25 21 24 sylbird ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L → e ∈ L → ∃ v ∈ V v I e
26 25 imp ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ∧ e ∈ L → ∃ v ∈ V v I e
27 df-ne ⊢ v ∈ V | v I e ≠ ∅ ↔ ¬ v ∈ V | v I e = ∅
28 rabn0 ⊢ v ∈ V | v I e ≠ ∅ ↔ ∃ v ∈ V v I e
29 27 28 bitr3i ⊢ ¬ v ∈ V | v I e = ∅ ↔ ∃ v ∈ V v I e
30 26 29 sylibr ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ∧ e ∈ L → ¬ v ∈ V | v I e = ∅
31 12 elsn ⊢ v ∈ V | v I e ∈ ∅ ↔ v ∈ V | v I e = ∅
32 30 31 sylnibr ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ∧ e ∈ L → ¬ v ∈ V | v I e ∈ ∅
33 19 32 eldifd ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L ∧ e ∈ L → v ∈ V | v I e ∈ 𝒫 V ∖ ∅
34 33 fmpttd ⊢ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L → e ∈ L ⟼ v ∈ V | v I e : L ⟶ 𝒫 V ∖ ∅
35 simpl ⊢ E = e ∈ L ⟼ v ∈ V | v I e ∧ dom ⁡ E = L → E = e ∈ L ⟼ v ∈ V | v I e
36 simpr ⊢ E = e ∈ L ⟼ v ∈ V | v I e ∧ dom ⁡ E = L → dom ⁡ E = L
37 35 36 feq12d ⊢ E = e ∈ L ⟼ v ∈ V | v I e ∧ dom ⁡ E = L → E : dom ⁡ E ⟶ 𝒫 V ∖ ∅ ↔ e ∈ L ⟼ v ∈ V | v I e : L ⟶ 𝒫 V ∖ ∅
38 34 37 imbitrrid ⊢ E = e ∈ L ⟼ v ∈ V | v I e ∧ dom ⁡ E = L → G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L → E : dom ⁡ E ⟶ 𝒫 V ∖ ∅
39 15 38 mpdan ⊢ E = e ∈ L ⟼ v ∈ V | v I e → G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L → E : dom ⁡ E ⟶ 𝒫 V ∖ ∅
40 39 imp ⊢ E = e ∈ L ⟼ v ∈ V | v I e ∧ G ∈ W ∧ I ⊆ V × L ∧ ran ⁡ I = L → E : dom ⁡ E ⟶ 𝒫 V ∖ ∅
41 9 40 biimtrrdi ⊢ V = P → E = e ∈ L ⟼ v ∈ P | v I e ∧ G ∈ W ∧ I ⊆ P × L ∧ ran ⁡ I = L → E : dom ⁡ E ⟶ 𝒫 V ∖ ∅
42 41 expdimp ⊢ V = P ∧ E = e ∈ L ⟼ v ∈ P | v I e → 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 | v I e → 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 | v I e → 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 | v I e → G ∈ UHGraph
48 47 ex ⊢ G ∈ W ∧ I ⊆ P × L ∧ ran ⁡ I = L → V = P ∧ E = e ∈ L ⟼ v ∈ P | v I e → G ∈ UHGraph