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 bitrid 
 |-  ( G e. U -> ( G e. USHGraph <-> E : dom E -1-1-> ( ~P V \ { (/) } ) ) )