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}=\mathrm{Vtx}\left({G}\right)$
incistruhgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
Assertion incistruhgr ${⊢}\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left(\left({V}={P}\wedge {E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)\to {G}\in \mathrm{UHGraph}\right)$

Proof

Step Hyp Ref Expression
1 incistruhgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 incistruhgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 rabeq ${⊢}{V}={P}\to \left\{{v}\in {V}|{v}{I}{e}\right\}=\left\{{v}\in {P}|{v}{I}{e}\right\}$
4 3 mpteq2dv ${⊢}{V}={P}\to \left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)$
5 4 eqeq2d ${⊢}{V}={P}\to \left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)↔{E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)$
6 xpeq1 ${⊢}{V}={P}\to {V}×{L}={P}×{L}$
7 6 sseq2d ${⊢}{V}={P}\to \left({I}\subseteq {V}×{L}↔{I}\subseteq {P}×{L}\right)$
8 7 3anbi2d ${⊢}{V}={P}\to \left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)↔\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\right)$
9 5 8 anbi12d ${⊢}{V}={P}\to \left(\left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\wedge \left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\right)↔\left({E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\wedge \left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\right)\right)$
10 dmeq ${⊢}{E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\to \mathrm{dom}{E}=\mathrm{dom}\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)$
11 1 fvexi ${⊢}{V}\in \mathrm{V}$
12 11 rabex ${⊢}\left\{{v}\in {V}|{v}{I}{e}\right\}\in \mathrm{V}$
13 eqid ${⊢}\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)$
14 12 13 dmmpti ${⊢}\mathrm{dom}\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)={L}$
15 10 14 syl6eq ${⊢}{E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\to \mathrm{dom}{E}={L}$
16 ssrab2 ${⊢}\left\{{v}\in {V}|{v}{I}{e}\right\}\subseteq {V}$
17 16 a1i ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge {e}\in {L}\right)\to \left\{{v}\in {V}|{v}{I}{e}\right\}\subseteq {V}$
18 12 elpw ${⊢}\left\{{v}\in {V}|{v}{I}{e}\right\}\in 𝒫{V}↔\left\{{v}\in {V}|{v}{I}{e}\right\}\subseteq {V}$
19 17 18 sylibr ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge {e}\in {L}\right)\to \left\{{v}\in {V}|{v}{I}{e}\right\}\in 𝒫{V}$
20 eleq2 ${⊢}\mathrm{ran}{I}={L}\to \left({e}\in \mathrm{ran}{I}↔{e}\in {L}\right)$
21 20 3ad2ant3 ${⊢}\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left({e}\in \mathrm{ran}{I}↔{e}\in {L}\right)$
22 ssrelrn ${⊢}\left({I}\subseteq {V}×{L}\wedge {e}\in \mathrm{ran}{I}\right)\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}$
23 22 ex ${⊢}{I}\subseteq {V}×{L}\to \left({e}\in \mathrm{ran}{I}\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}\right)$
24 23 3ad2ant2 ${⊢}\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left({e}\in \mathrm{ran}{I}\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}\right)$
25 21 24 sylbird ${⊢}\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left({e}\in {L}\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}\right)$
26 25 imp ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge {e}\in {L}\right)\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}$
27 df-ne ${⊢}\left\{{v}\in {V}|{v}{I}{e}\right\}\ne \varnothing ↔¬\left\{{v}\in {V}|{v}{I}{e}\right\}=\varnothing$
28 rabn0 ${⊢}\left\{{v}\in {V}|{v}{I}{e}\right\}\ne \varnothing ↔\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}$
29 27 28 bitr3i ${⊢}¬\left\{{v}\in {V}|{v}{I}{e}\right\}=\varnothing ↔\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{v}{I}{e}$
30 26 29 sylibr ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge {e}\in {L}\right)\to ¬\left\{{v}\in {V}|{v}{I}{e}\right\}=\varnothing$
31 12 elsn ${⊢}\left\{{v}\in {V}|{v}{I}{e}\right\}\in \left\{\varnothing \right\}↔\left\{{v}\in {V}|{v}{I}{e}\right\}=\varnothing$
32 30 31 sylnibr ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge {e}\in {L}\right)\to ¬\left\{{v}\in {V}|{v}{I}{e}\right\}\in \left\{\varnothing \right\}$
33 19 32 eldifd ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge {e}\in {L}\right)\to \left\{{v}\in {V}|{v}{I}{e}\right\}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)$
34 33 fmpttd ${⊢}\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right):{L}⟶𝒫{V}\setminus \left\{\varnothing \right\}$
35 simpl ${⊢}\left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\wedge \mathrm{dom}{E}={L}\right)\to {E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)$
36 simpr ${⊢}\left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\wedge \mathrm{dom}{E}={L}\right)\to \mathrm{dom}{E}={L}$
37 35 36 feq12d ${⊢}\left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\wedge \mathrm{dom}{E}={L}\right)\to \left({E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}↔\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right):{L}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
38 34 37 syl5ibr ${⊢}\left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\wedge \mathrm{dom}{E}={L}\right)\to \left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
39 15 38 mpdan ${⊢}{E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\to \left(\left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
40 39 imp ${⊢}\left({E}=\left({e}\in {L}⟼\left\{{v}\in {V}|{v}{I}{e}\right\}\right)\wedge \left({G}\in {W}\wedge {I}\subseteq {V}×{L}\wedge \mathrm{ran}{I}={L}\right)\right)\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}$
41 9 40 syl6bir ${⊢}{V}={P}\to \left(\left({E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\wedge \left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\right)\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
42 41 expdimp ${⊢}\left({V}={P}\wedge {E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)\to \left(\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
43 42 impcom ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge \left({V}={P}\wedge {E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)\right)\to {E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}$
44 1 2 isuhgr ${⊢}{G}\in {W}\to \left({G}\in \mathrm{UHGraph}↔{E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
45 44 3ad2ant1 ${⊢}\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left({G}\in \mathrm{UHGraph}↔{E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
46 45 adantr ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge \left({V}={P}\wedge {E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)\right)\to \left({G}\in \mathrm{UHGraph}↔{E}:\mathrm{dom}{E}⟶𝒫{V}\setminus \left\{\varnothing \right\}\right)$
47 43 46 mpbird ${⊢}\left(\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\wedge \left({V}={P}\wedge {E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)\right)\to {G}\in \mathrm{UHGraph}$
48 47 ex ${⊢}\left({G}\in {W}\wedge {I}\subseteq {P}×{L}\wedge \mathrm{ran}{I}={L}\right)\to \left(\left({V}={P}\wedge {E}=\left({e}\in {L}⟼\left\{{v}\in {P}|{v}{I}{e}\right\}\right)\right)\to {G}\in \mathrm{UHGraph}\right)$