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 𝑉 = ( Vtx ‘ 𝐺 )
incistruhgr.e 𝐸 = ( iEdg ‘ 𝐺 )
Assertion incistruhgr ( ( 𝐺𝑊𝐼 ⊆ ( 𝑃 × 𝐿 ) ∧ ran 𝐼 = 𝐿 ) → ( ( 𝑉 = 𝑃𝐸 = ( 𝑒𝐿 ↦ { 𝑣𝑃𝑣 𝐼 𝑒 } ) ) → 𝐺 ∈ UHGraph ) )

Proof

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