Metamath Proof Explorer


Theorem isushgr

Description: The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020) (Revised by AV, 9-Oct-2020)

Ref Expression
Hypotheses isuhgr.v
|- V = ( Vtx ` G )
isuhgr.e
|- E = ( iEdg ` G )
Assertion isushgr
|- ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )

Proof

Step Hyp Ref Expression
1 isuhgr.v
 |-  V = ( Vtx ` G )
2 isuhgr.e
 |-  E = ( iEdg ` G )
3 df-ushgr
 |-  USHGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) }
4 3 eleq2i
 |-  ( G e. USHGraph <-> G e. { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e -1-1-> ( ~P v \ { (/) } ) } )
5 fveq2
 |-  ( h = G -> ( iEdg ` h ) = ( iEdg ` G ) )
6 5 2 eqtr4di
 |-  ( h = G -> ( iEdg ` h ) = E )
7 5 dmeqd
 |-  ( h = G -> dom ( iEdg ` h ) = dom ( iEdg ` G ) )
8 2 eqcomi
 |-  ( iEdg ` G ) = E
9 8 dmeqi
 |-  dom ( iEdg ` G ) = dom E
10 7 9 eqtrdi
 |-  ( h = G -> dom ( iEdg ` h ) = dom E )
11 fveq2
 |-  ( h = G -> ( Vtx ` h ) = ( Vtx ` G ) )
12 11 1 eqtr4di
 |-  ( h = G -> ( Vtx ` h ) = V )
13 12 pweqd
 |-  ( h = G -> ~P ( Vtx ` h ) = ~P V )
14 13 difeq1d
 |-  ( h = G -> ( ~P ( Vtx ` h ) \ { (/) } ) = ( ~P V \ { (/) } ) )
15 6 10 14 f1eq123d
 |-  ( h = G -> ( ( iEdg ` h ) : dom ( iEdg ` h ) -1-1-> ( ~P ( Vtx ` h ) \ { (/) } ) <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )
16 fvexd
 |-  ( g = h -> ( Vtx ` g ) e. _V )
17 fveq2
 |-  ( g = h -> ( Vtx ` g ) = ( Vtx ` h ) )
18 fvexd
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ( iEdg ` g ) e. _V )
19 fveq2
 |-  ( g = h -> ( iEdg ` g ) = ( iEdg ` h ) )
20 19 adantr
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ( iEdg ` g ) = ( iEdg ` h ) )
21 simpr
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> e = ( iEdg ` h ) )
22 21 dmeqd
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> dom e = dom ( iEdg ` h ) )
23 simpr
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> v = ( Vtx ` h ) )
24 23 pweqd
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ~P v = ~P ( Vtx ` h ) )
25 24 difeq1d
 |-  ( ( g = h /\ v = ( Vtx ` h ) ) -> ( ~P v \ { (/) } ) = ( ~P ( Vtx ` h ) \ { (/) } ) )
26 25 adantr
 |-  ( ( ( g = h /\ v = ( Vtx ` h ) ) /\ e = ( iEdg ` h ) ) -> ( ~P v \ { (/) } ) = ( ~P ( Vtx ` h ) \ { (/) } ) )
27 21 22 26 f1eq123d
 |-  ( ( ( 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 ) \ { (/) } ) ) )
28 18 20 27 sbcied2
 |-  ( ( 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 ) \ { (/) } ) ) )
29 16 17 28 sbcied2
 |-  ( 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 ) \ { (/) } ) ) )
30 29 cbvabv
 |-  { 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 ) \ { (/) } ) }
31 15 30 elab2g
 |-  ( 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 \ { (/) } ) ) )
32 4 31 syl5bb
 |-  ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )