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

Theorem isushgr 39152
Description: The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.)
Hypotheses
Ref Expression
isuhgr.v  |-  V  =  (Vtx `  G )
isuhgr.e  |-  E  =  (iEdg `  G )
Assertion
Ref Expression
isushgr  |-  ( G  e.  U  ->  ( G  e. USHGraph  <->  E : dom  E -1-1-> ( ~P V  \  { (/)
} ) ) )

Proof of Theorem isushgr
Dummy variables  g  h  v  e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ushgr 39150 . . 3  |- USHGraph  =  {
g  |  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/)
} ) }
21eleq2i 2521 . 2  |-  ( G  e. USHGraph 
<->  G  e.  { g  |  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/)
} ) } )
3 fveq2 5865 . . . . 5  |-  ( h  =  G  ->  (iEdg `  h )  =  (iEdg `  G ) )
4 isuhgr.e . . . . 5  |-  E  =  (iEdg `  G )
53, 4syl6eqr 2503 . . . 4  |-  ( h  =  G  ->  (iEdg `  h )  =  E )
63dmeqd 5037 . . . . 5  |-  ( h  =  G  ->  dom  (iEdg `  h )  =  dom  (iEdg `  G
) )
74eqcomi 2460 . . . . . 6  |-  (iEdg `  G )  =  E
87dmeqi 5036 . . . . 5  |-  dom  (iEdg `  G )  =  dom  E
96, 8syl6eq 2501 . . . 4  |-  ( h  =  G  ->  dom  (iEdg `  h )  =  dom  E )
10 fveq2 5865 . . . . . . 7  |-  ( h  =  G  ->  (Vtx `  h )  =  (Vtx
`  G ) )
11 isuhgr.v . . . . . . 7  |-  V  =  (Vtx `  G )
1210, 11syl6eqr 2503 . . . . . 6  |-  ( h  =  G  ->  (Vtx `  h )  =  V )
1312pweqd 3956 . . . . 5  |-  ( h  =  G  ->  ~P (Vtx `  h )  =  ~P V )
1413difeq1d 3550 . . . 4  |-  ( h  =  G  ->  ( ~P (Vtx `  h )  \  { (/) } )  =  ( ~P V  \  { (/) } ) )
155, 9, 14f1eq123d 5809 . . 3  |-  ( h  =  G  ->  (
(iEdg `  h ) : dom  (iEdg `  h
) -1-1-> ( ~P (Vtx `  h )  \  { (/)
} )  <->  E : dom  E -1-1-> ( ~P V  \  { (/) } ) ) )
16 fvex 5875 . . . . . 6  |-  (Vtx `  g )  e.  _V
1716a1i 11 . . . . 5  |-  ( g  =  h  ->  (Vtx `  g )  e.  _V )
18 fveq2 5865 . . . . 5  |-  ( g  =  h  ->  (Vtx `  g )  =  (Vtx
`  h ) )
19 fvex 5875 . . . . . . 7  |-  (iEdg `  g )  e.  _V
2019a1i 11 . . . . . 6  |-  ( ( g  =  h  /\  v  =  (Vtx `  h
) )  ->  (iEdg `  g )  e.  _V )
21 fveq2 5865 . . . . . . 7  |-  ( g  =  h  ->  (iEdg `  g )  =  (iEdg `  h ) )
2221adantr 467 . . . . . 6  |-  ( ( g  =  h  /\  v  =  (Vtx `  h
) )  ->  (iEdg `  g )  =  (iEdg `  h ) )
23 simpr 463 . . . . . . 7  |-  ( ( ( g  =  h  /\  v  =  (Vtx
`  h ) )  /\  e  =  (iEdg `  h ) )  -> 
e  =  (iEdg `  h ) )
2423dmeqd 5037 . . . . . . 7  |-  ( ( ( g  =  h  /\  v  =  (Vtx
`  h ) )  /\  e  =  (iEdg `  h ) )  ->  dom  e  =  dom  (iEdg `  h ) )
25 simpr 463 . . . . . . . . . 10  |-  ( ( g  =  h  /\  v  =  (Vtx `  h
) )  ->  v  =  (Vtx `  h )
)
2625pweqd 3956 . . . . . . . . 9  |-  ( ( g  =  h  /\  v  =  (Vtx `  h
) )  ->  ~P v  =  ~P (Vtx `  h ) )
2726difeq1d 3550 . . . . . . . 8  |-  ( ( g  =  h  /\  v  =  (Vtx `  h
) )  ->  ( ~P v  \  { (/) } )  =  ( ~P (Vtx `  h )  \  { (/) } ) )
2827adantr 467 . . . . . . 7  |-  ( ( ( g  =  h  /\  v  =  (Vtx
`  h ) )  /\  e  =  (iEdg `  h ) )  -> 
( ~P v  \  { (/) } )  =  ( ~P (Vtx `  h )  \  { (/)
} ) )
2923, 24, 28f1eq123d 5809 . . . . . 6  |-  ( ( ( g  =  h  /\  v  =  (Vtx
`  h ) )  /\  e  =  (iEdg `  h ) )  -> 
( e : dom  e -1-1-> ( ~P v  \  { (/) } )  <->  (iEdg `  h
) : dom  (iEdg `  h ) -1-1-> ( ~P (Vtx `  h )  \  { (/) } ) ) )
3020, 22, 29sbcied2 3305 . . . . 5  |-  ( ( g  =  h  /\  v  =  (Vtx `  h
) )  ->  ( [. (iEdg `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } )  <->  (iEdg `  h ) : dom  (iEdg `  h
) -1-1-> ( ~P (Vtx `  h )  \  { (/)
} ) ) )
3117, 18, 30sbcied2 3305 . . . 4  |-  ( g  =  h  ->  ( [. (Vtx `  g )  /  v ]. [. (iEdg `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } )  <->  (iEdg `  h
) : dom  (iEdg `  h ) -1-1-> ( ~P (Vtx `  h )  \  { (/) } ) ) )
3231cbvabv 2575 . . 3  |-  { g  |  [. (Vtx `  g )  /  v ]. [. (iEdg `  g
)  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/)
} ) }  =  { h  |  (iEdg `  h ) : dom  (iEdg `  h ) -1-1-> ( ~P (Vtx `  h
)  \  { (/) } ) }
3315, 32elab2g 3187 . 2  |-  ( G  e.  U  ->  ( G  e.  { g  |  [. (Vtx `  g
)  /  v ]. [. (iEdg `  g )  /  e ]. e : dom  e -1-1-> ( ~P v  \  { (/) } ) }  <->  E : dom  E -1-1-> ( ~P V  \  { (/) } ) ) )
342, 33syl5bb 261 1  |-  ( G  e.  U  ->  ( G  e. USHGraph  <->  E : dom  E -1-1-> ( ~P V  \  { (/)
} ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444    e. wcel 1887   {cab 2437   _Vcvv 3045   [.wsbc 3267    \ cdif 3401   (/)c0 3731   ~Pcpw 3951   {csn 3968   dom cdm 4834   -1-1->wf1 5579   ` cfv 5582  Vtxcvtx 39101  iEdgciedg 39102   USHGraph cushgr 39148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-nul 4534
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fv 5590  df-ushgr 39150
This theorem is referenced by:  ushgrf  39154  uspgrushgr  39262
  Copyright terms: Public domain W3C validator