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

Theorem incistruhgr 39181
Description: An incident structure  <. P ,  L ,  I >. "where  P is a set whose elements are called points,  L is a distinct set whose elements are called lines and  I  C_  ( P  X.  L ) 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  P  =  (
Base `  S ) 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  |-  V  =  (Vtx `  G )
incistruhgr.e  |-  E  =  (iEdg `  G )
Assertion
Ref Expression
incistruhgr  |-  ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  ->  ( ( V  =  P  /\  E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) )  ->  G  e. UHGraph  ) )
Distinct variable groups:    e, E    e, G    e, I, v   
e, L, v    P, e, v    e, V, v   
e, W
Allowed substitution hints:    E( v)    G( v)    W( v)

Proof of Theorem incistruhgr
StepHypRef Expression
1 id 22 . . . . . . . . . 10  |-  ( V  =  P  ->  V  =  P )
21rabeqdv 3041 . . . . . . . . 9  |-  ( V  =  P  ->  { v  e.  V  |  v I e }  =  { v  e.  P  |  v I e } )
32mpteq2dv 4493 . . . . . . . 8  |-  ( V  =  P  ->  (
e  e.  L  |->  { v  e.  V  | 
v I e } )  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) )
43eqeq2d 2463 . . . . . . 7  |-  ( V  =  P  ->  ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  <-> 
E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) ) )
5 xpeq1 4851 . . . . . . . . 9  |-  ( V  =  P  ->  ( V  X.  L )  =  ( P  X.  L
) )
65sseq2d 3462 . . . . . . . 8  |-  ( V  =  P  ->  (
I  C_  ( V  X.  L )  <->  I  C_  ( P  X.  L ) ) )
763anbi2d 1346 . . . . . . 7  |-  ( V  =  P  ->  (
( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  <-> 
( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L ) ) )
84, 7anbi12d 718 . . . . . 6  |-  ( V  =  P  ->  (
( E  =  ( e  e.  L  |->  { v  e.  V  | 
v I e } )  /\  ( G  e.  W  /\  I  C_  ( V  X.  L
)  /\  ran  I  =  L ) )  <->  ( E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } )  /\  ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L ) ) ) )
9 dmeq 5038 . . . . . . . . 9  |-  ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  ->  dom  E  =  dom  (
e  e.  L  |->  { v  e.  V  | 
v I e } ) )
10 incistruhgr.v . . . . . . . . . . . . 13  |-  V  =  (Vtx `  G )
11 fvex 5880 . . . . . . . . . . . . 13  |-  (Vtx `  G )  e.  _V
1210, 11eqeltri 2527 . . . . . . . . . . . 12  |-  V  e. 
_V
1312rabex 4557 . . . . . . . . . . 11  |-  { v  e.  V  |  v I e }  e.  _V
14 eqid 2453 . . . . . . . . . . 11  |-  ( e  e.  L  |->  { v  e.  V  |  v I e } )  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )
1513, 14dmmpti 5712 . . . . . . . . . 10  |-  dom  (
e  e.  L  |->  { v  e.  V  | 
v I e } )  =  L
1615a1i 11 . . . . . . . . 9  |-  ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  ->  dom  ( e  e.  L  |->  { v  e.  V  |  v I e } )  =  L )
179, 16eqtrd 2487 . . . . . . . 8  |-  ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  ->  dom  E  =  L )
18 ssrab2 3516 . . . . . . . . . . . . 13  |-  { v  e.  V  |  v I e }  C_  V
1918a1i 11 . . . . . . . . . . . 12  |-  ( ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  /\  e  e.  L
)  ->  { v  e.  V  |  v
I e }  C_  V )
2013elpw 3959 . . . . . . . . . . . 12  |-  ( { v  e.  V  | 
v I e }  e.  ~P V  <->  { v  e.  V  |  v
I e }  C_  V )
2119, 20sylibr 216 . . . . . . . . . . 11  |-  ( ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  /\  e  e.  L
)  ->  { v  e.  V  |  v
I e }  e.  ~P V )
22 eleq2 2520 . . . . . . . . . . . . . . . 16  |-  ( ran  I  =  L  -> 
( e  e.  ran  I 
<->  e  e.  L ) )
23223ad2ant3 1032 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  ->  ( e  e.  ran  I 
<->  e  e.  L ) )
24 ssrelrn 39022 . . . . . . . . . . . . . . . . 17  |-  ( ( I  C_  ( V  X.  L )  /\  e  e.  ran  I )  ->  E. v  e.  V  v I e )
2524ex 436 . . . . . . . . . . . . . . . 16  |-  ( I 
C_  ( V  X.  L )  ->  (
e  e.  ran  I  ->  E. v  e.  V  v I e ) )
26253ad2ant2 1031 . . . . . . . . . . . . . . 15  |-  ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  ->  ( e  e.  ran  I  ->  E. v  e.  V  v I e ) )
2723, 26sylbird 239 . . . . . . . . . . . . . 14  |-  ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  ->  ( e  e.  L  ->  E. v  e.  V  v I e ) )
2827imp 431 . . . . . . . . . . . . 13  |-  ( ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  /\  e  e.  L
)  ->  E. v  e.  V  v I
e )
29 df-ne 2626 . . . . . . . . . . . . . 14  |-  ( { v  e.  V  | 
v I e }  =/=  (/)  <->  -.  { v  e.  V  |  v
I e }  =  (/) )
30 rabn0 3754 . . . . . . . . . . . . . 14  |-  ( { v  e.  V  | 
v I e }  =/=  (/)  <->  E. v  e.  V  v I e )
3129, 30bitr3i 255 . . . . . . . . . . . . 13  |-  ( -. 
{ v  e.  V  |  v I e }  =  (/)  <->  E. v  e.  V  v I
e )
3228, 31sylibr 216 . . . . . . . . . . . 12  |-  ( ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  /\  e  e.  L
)  ->  -.  { v  e.  V  |  v I e }  =  (/) )
3313elsnc 3994 . . . . . . . . . . . 12  |-  ( { v  e.  V  | 
v I e }  e.  { (/) }  <->  { v  e.  V  |  v
I e }  =  (/) )
3432, 33sylnibr 307 . . . . . . . . . . 11  |-  ( ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  /\  e  e.  L
)  ->  -.  { v  e.  V  |  v I e }  e.  {
(/) } )
3521, 34eldifd 3417 . . . . . . . . . 10  |-  ( ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  /\  e  e.  L
)  ->  { v  e.  V  |  v
I e }  e.  ( ~P V  \  { (/)
} ) )
3635, 14fmptd 6051 . . . . . . . . 9  |-  ( ( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  ->  ( e  e.  L  |->  { v  e.  V  |  v I e } ) : L --> ( ~P V  \  { (/)
} ) )
37 simpl 459 . . . . . . . . . 10  |-  ( ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  /\  dom  E  =  L )  ->  E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } ) )
38 simpr 463 . . . . . . . . . 10  |-  ( ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  /\  dom  E  =  L )  ->  dom  E  =  L )
3937, 38feq12d 5722 . . . . . . . . 9  |-  ( ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  /\  dom  E  =  L )  ->  ( E : dom  E --> ( ~P V  \  { (/) } )  <->  ( e  e.  L  |->  { v  e.  V  |  v I e } ) : L --> ( ~P V  \  { (/) } ) ) )
4036, 39syl5ibr 225 . . . . . . . 8  |-  ( ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  /\  dom  E  =  L )  ->  (
( G  e.  W  /\  I  C_  ( V  X.  L )  /\  ran  I  =  L )  ->  E : dom  E --> ( ~P V  \  { (/) } ) ) )
4117, 40mpdan 675 . . . . . . 7  |-  ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  -> 
( ( G  e.  W  /\  I  C_  ( V  X.  L
)  /\  ran  I  =  L )  ->  E : dom  E --> ( ~P V  \  { (/) } ) ) )
4241imp 431 . . . . . 6  |-  ( ( E  =  ( e  e.  L  |->  { v  e.  V  |  v I e } )  /\  ( G  e.  W  /\  I  C_  ( V  X.  L
)  /\  ran  I  =  L ) )  ->  E : dom  E --> ( ~P V  \  { (/) } ) )
438, 42syl6bir 233 . . . . 5  |-  ( V  =  P  ->  (
( E  =  ( e  e.  L  |->  { v  e.  P  | 
v I e } )  /\  ( G  e.  W  /\  I  C_  ( P  X.  L
)  /\  ran  I  =  L ) )  ->  E : dom  E --> ( ~P V  \  { (/) } ) ) )
4443expdimp 439 . . . 4  |-  ( ( V  =  P  /\  E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) )  ->  ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  ->  E : dom  E --> ( ~P V  \  { (/)
} ) ) )
4544impcom 432 . . 3  |-  ( ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  /\  ( V  =  P  /\  E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) ) )  ->  E : dom  E --> ( ~P V  \  { (/) } ) )
46 incistruhgr.e . . . . . 6  |-  E  =  (iEdg `  G )
4710, 46isuhgr 39161 . . . . 5  |-  ( G  e.  W  ->  ( G  e. UHGraph  <->  E : dom  E --> ( ~P V  \  { (/)
} ) ) )
48473ad2ant1 1030 . . . 4  |-  ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  ->  ( G  e. UHGraph  <->  E : dom  E --> ( ~P V  \  { (/) } ) ) )
4948adantr 467 . . 3  |-  ( ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  /\  ( V  =  P  /\  E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) ) )  ->  ( G  e. UHGraph  <->  E : dom  E --> ( ~P V  \  { (/) } ) ) )
5045, 49mpbird 236 . 2  |-  ( ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  /\  ( V  =  P  /\  E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) ) )  ->  G  e. UHGraph  )
5150ex 436 1  |-  ( ( G  e.  W  /\  I  C_  ( P  X.  L )  /\  ran  I  =  L )  ->  ( ( V  =  P  /\  E  =  ( e  e.  L  |->  { v  e.  P  |  v I e } ) )  ->  G  e. UHGraph  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 986    = wceq 1446    e. wcel 1889    =/= wne 2624   E.wrex 2740   {crab 2743   _Vcvv 3047    \ cdif 3403    C_ wss 3406   (/)c0 3733   ~Pcpw 3953   {csn 3970   class class class wbr 4405    |-> cmpt 4464    X. cxp 4835   dom cdm 4837   ran crn 4838   -->wf 5581   ` cfv 5585  Vtxcvtx 39111  iEdgciedg 39112   UHGraph cuhgr 39157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-uhgr 39159
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator