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 ) )