This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uhgreq12g

Description: If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017) (Revised by AV, 18-Jan-2020)

Ref Expression
Hypotheses uhgrf.v 
|- V = ( Vtx ` G )
uhgrf.e 
|- E = ( iEdg ` G )
uhgreq12g.w 
|- W = ( Vtx ` H )
uhgreq12g.f 
|- F = ( iEdg ` H )
Assertion uhgreq12g 
|- ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> H e. UHGraph ) )

Proof

Step Hyp Ref Expression
1 uhgrf.v 
 |-  V = ( Vtx ` G )
2 uhgrf.e 
 |-  E = ( iEdg ` G )
3 uhgreq12g.w 
 |-  W = ( Vtx ` H )
4 uhgreq12g.f 
 |-  F = ( iEdg ` H )
5 1 2 isuhgr 
 |-  ( G e. X -> ( G e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )
6 5 adantr 
 |-  ( ( G e. X /\ H e. Y ) -> ( G e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )
7 6 adantr 
 |-  ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) )
8 simpr 
 |-  ( ( V = W /\ E = F ) -> E = F )
9 8 dmeqd 
 |-  ( ( V = W /\ E = F ) -> dom E = dom F )
10 pweq 
 |-  ( V = W -> ~P V = ~P W )
11 10 difeq1d 
 |-  ( V = W -> ( ~P V \ { (/) } ) = ( ~P W \ { (/) } ) )
12 11 adantr 
 |-  ( ( V = W /\ E = F ) -> ( ~P V \ { (/) } ) = ( ~P W \ { (/) } ) )
13 8 9 12 feq123d 
 |-  ( ( V = W /\ E = F ) -> ( E : dom E --> ( ~P V \ { (/) } ) <-> F : dom F --> ( ~P W \ { (/) } ) ) )
14 3 4 isuhgr 
 |-  ( H e. Y -> ( H e. UHGraph <-> F : dom F --> ( ~P W \ { (/) } ) ) )
15 14 adantl 
 |-  ( ( G e. X /\ H e. Y ) -> ( H e. UHGraph <-> F : dom F --> ( ~P W \ { (/) } ) ) )
16 15 bicomd 
 |-  ( ( G e. X /\ H e. Y ) -> ( F : dom F --> ( ~P W \ { (/) } ) <-> H e. UHGraph ) )
17 13 16 sylan9bbr 
 |-  ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( E : dom E --> ( ~P V \ { (/) } ) <-> H e. UHGraph ) )
18 7 17 bitrd 
 |-  ( ( ( G e. X /\ H e. Y ) /\ ( V = W /\ E = F ) ) -> ( G e. UHGraph <-> H e. UHGraph ) )