Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  incistruhgr Structured version   Visualization version   GIF version

Theorem incistruhgr 40286
Description: An incident structure 𝑃, 𝐿, 𝐼 "where 𝑃 is a set whose elements are called points, 𝐿 is a distinct set whose elements are called lines and 𝐼 ⊆ (𝑃 × 𝐿) is the incidence 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 𝑃 = (Base‘𝑆) 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 incident structure is 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.)
Hypotheses
Ref Expression
incistruhgr.v 𝑉 = (Vtx‘𝐺)
incistruhgr.e 𝐸 = (iEdg‘𝐺)
Assertion
Ref Expression
incistruhgr ((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph ))
Distinct variable groups:   𝑒,𝐸   𝑒,𝐺   𝑒,𝐼,𝑣   𝑒,𝐿,𝑣   𝑃,𝑒,𝑣   𝑒,𝑉,𝑣   𝑒,𝑊
Allowed substitution hints:   𝐸(𝑣)   𝐺(𝑣)   𝑊(𝑣)

Proof of Theorem incistruhgr
StepHypRef Expression
1 id 22 . . . . . . . . . 10 (𝑉 = 𝑃𝑉 = 𝑃)
21rabeqdv 3166 . . . . . . . . 9 (𝑉 = 𝑃 → {𝑣𝑉𝑣𝐼𝑒} = {𝑣𝑃𝑣𝐼𝑒})
32mpteq2dv 4667 . . . . . . . 8 (𝑉 = 𝑃 → (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒}))
43eqeq2d 2619 . . . . . . 7 (𝑉 = 𝑃 → (𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ↔ 𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒})))
5 xpeq1 5041 . . . . . . . . 9 (𝑉 = 𝑃 → (𝑉 × 𝐿) = (𝑃 × 𝐿))
65sseq2d 3595 . . . . . . . 8 (𝑉 = 𝑃 → (𝐼 ⊆ (𝑉 × 𝐿) ↔ 𝐼 ⊆ (𝑃 × 𝐿)))
763anbi2d 1395 . . . . . . 7 (𝑉 = 𝑃 → ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ↔ (𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿)))
84, 7anbi12d 742 . . . . . 6 (𝑉 = 𝑃 → ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ∧ (𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿)) ↔ (𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒}) ∧ (𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿))))
9 dmeq 5232 . . . . . . . . 9 (𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) → dom 𝐸 = dom (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}))
10 incistruhgr.v . . . . . . . . . . . . 13 𝑉 = (Vtx‘𝐺)
11 fvex 6097 . . . . . . . . . . . . 13 (Vtx‘𝐺) ∈ V
1210, 11eqeltri 2683 . . . . . . . . . . . 12 𝑉 ∈ V
1312rabex 4734 . . . . . . . . . . 11 {𝑣𝑉𝑣𝐼𝑒} ∈ V
14 eqid 2609 . . . . . . . . . . 11 (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒})
1513, 14dmmpti 5921 . . . . . . . . . 10 dom (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) = 𝐿
1615a1i 11 . . . . . . . . 9 (𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) → dom (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) = 𝐿)
179, 16eqtrd 2643 . . . . . . . 8 (𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) → dom 𝐸 = 𝐿)
18 ssrab2 3649 . . . . . . . . . . . . 13 {𝑣𝑉𝑣𝐼𝑒} ⊆ 𝑉
1918a1i 11 . . . . . . . . . . . 12 (((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒𝐿) → {𝑣𝑉𝑣𝐼𝑒} ⊆ 𝑉)
2013elpw 4113 . . . . . . . . . . . 12 ({𝑣𝑉𝑣𝐼𝑒} ∈ 𝒫 𝑉 ↔ {𝑣𝑉𝑣𝐼𝑒} ⊆ 𝑉)
2119, 20sylibr 222 . . . . . . . . . . 11 (((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒𝐿) → {𝑣𝑉𝑣𝐼𝑒} ∈ 𝒫 𝑉)
22 eleq2 2676 . . . . . . . . . . . . . . . 16 (ran 𝐼 = 𝐿 → (𝑒 ∈ ran 𝐼𝑒𝐿))
23223ad2ant3 1076 . . . . . . . . . . . . . . 15 ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒 ∈ ran 𝐼𝑒𝐿))
24 ssrelrn 40115 . . . . . . . . . . . . . . . . 17 ((𝐼 ⊆ (𝑉 × 𝐿) ∧ 𝑒 ∈ ran 𝐼) → ∃𝑣𝑉 𝑣𝐼𝑒)
2524ex 448 . . . . . . . . . . . . . . . 16 (𝐼 ⊆ (𝑉 × 𝐿) → (𝑒 ∈ ran 𝐼 → ∃𝑣𝑉 𝑣𝐼𝑒))
26253ad2ant2 1075 . . . . . . . . . . . . . . 15 ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒 ∈ ran 𝐼 → ∃𝑣𝑉 𝑣𝐼𝑒))
2723, 26sylbird 248 . . . . . . . . . . . . . 14 ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒𝐿 → ∃𝑣𝑉 𝑣𝐼𝑒))
2827imp 443 . . . . . . . . . . . . 13 (((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒𝐿) → ∃𝑣𝑉 𝑣𝐼𝑒)
29 df-ne 2781 . . . . . . . . . . . . . 14 ({𝑣𝑉𝑣𝐼𝑒} ≠ ∅ ↔ ¬ {𝑣𝑉𝑣𝐼𝑒} = ∅)
30 rabn0 3911 . . . . . . . . . . . . . 14 ({𝑣𝑉𝑣𝐼𝑒} ≠ ∅ ↔ ∃𝑣𝑉 𝑣𝐼𝑒)
3129, 30bitr3i 264 . . . . . . . . . . . . 13 (¬ {𝑣𝑉𝑣𝐼𝑒} = ∅ ↔ ∃𝑣𝑉 𝑣𝐼𝑒)
3228, 31sylibr 222 . . . . . . . . . . . 12 (((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒𝐿) → ¬ {𝑣𝑉𝑣𝐼𝑒} = ∅)
3313elsn 4139 . . . . . . . . . . . 12 ({𝑣𝑉𝑣𝐼𝑒} ∈ {∅} ↔ {𝑣𝑉𝑣𝐼𝑒} = ∅)
3432, 33sylnibr 317 . . . . . . . . . . 11 (((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒𝐿) → ¬ {𝑣𝑉𝑣𝐼𝑒} ∈ {∅})
3521, 34eldifd 3550 . . . . . . . . . 10 (((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ 𝑒𝐿) → {𝑣𝑉𝑣𝐼𝑒} ∈ (𝒫 𝑉 ∖ {∅}))
3635, 14fmptd 6276 . . . . . . . . 9 ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}):𝐿⟶(𝒫 𝑉 ∖ {∅}))
37 simpl 471 . . . . . . . . . 10 ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → 𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}))
38 simpr 475 . . . . . . . . . 10 ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → dom 𝐸 = 𝐿)
3937, 38feq12d 5931 . . . . . . . . 9 ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}):𝐿⟶(𝒫 𝑉 ∖ {∅})))
4036, 39syl5ibr 234 . . . . . . . 8 ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ∧ dom 𝐸 = 𝐿) → ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
4117, 40mpdan 698 . . . . . . 7 (𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) → ((𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
4241imp 443 . . . . . 6 ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑉𝑣𝐼𝑒}) ∧ (𝐺𝑊𝐼 ⊆ (𝑉 × 𝐿) ∧ ran 𝐼 = 𝐿)) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))
438, 42syl6bir 242 . . . . 5 (𝑉 = 𝑃 → ((𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒}) ∧ (𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿)) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
4443expdimp 451 . . . 4 ((𝑉 = 𝑃𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒})) → ((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
4544impcom 444 . . 3 (((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ (𝑉 = 𝑃𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒}))) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))
46 incistruhgr.e . . . . . 6 𝐸 = (iEdg‘𝐺)
4710, 46isuhgr 40263 . . . . 5 (𝐺𝑊 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
48473ad2ant1 1074 . . . 4 ((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
4948adantr 479 . . 3 (((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ (𝑉 = 𝑃𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒}))) → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))
5045, 49mpbird 245 . 2 (((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) ∧ (𝑉 = 𝑃𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒}))) → 𝐺 ∈ UHGraph )
5150ex 448 1 ((𝐺𝑊𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃𝐸 = (𝑒𝐿 ↦ {𝑣𝑃𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wrex 2896  {crab 2899  Vcvv 3172  cdif 3536  wss 3539  c0 3873  𝒫 cpw 4107  {csn 4124   class class class wbr 4577  cmpt 4637   × cxp 5025  dom cdm 5027  ran crn 5028  wf 5785  cfv 5789  Vtxcvtx 40210  iEdgciedg 40211   UHGraph cuhgr 40259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-fv 5797  df-uhgr 40261
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator