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∈X∧H∈Y∧V=W∧E=F→G∈UHGraph↔H∈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∈X→G∈UHGraph↔E:dom⁡E⟶𝒫V∖∅
6 5 adantr ⊢G∈X∧H∈Y→G∈UHGraph↔E:dom⁡E⟶𝒫V∖∅
7 6 adantr ⊢G∈X∧H∈Y∧V=W∧E=F→G∈UHGraph↔E:dom⁡E⟶𝒫V∖∅
8 simpr ⊢V=W∧E=F→E=F
9 8 dmeqd ⊢V=W∧E=F→dom⁡E=dom⁡F
10 pweq ⊢V=W→𝒫V=𝒫W
11 10 difeq1d ⊢V=W→𝒫V∖∅=𝒫W∖∅
12 11 adantr ⊢V=W∧E=F→𝒫V∖∅=𝒫W∖∅
13 8 9 12 feq123d ⊢V=W∧E=F→E:dom⁡E⟶𝒫V∖∅↔F:dom⁡F⟶𝒫W∖∅
14 3 4 isuhgr ⊢H∈Y→H∈UHGraph↔F:dom⁡F⟶𝒫W∖∅
15 14 adantl ⊢G∈X∧H∈Y→H∈UHGraph↔F:dom⁡F⟶𝒫W∖∅
16 15 bicomd ⊢G∈X∧H∈Y→F:dom⁡F⟶𝒫W∖∅↔H∈UHGraph
17 13 16 sylan9bbr ⊢G∈X∧H∈Y∧V=W∧E=F→E:dom⁡E⟶𝒫V∖∅↔H∈UHGraph
18 7 17 bitrd ⊢G∈X∧H∈Y∧V=W∧E=F→G∈UHGraph↔H∈UHGraph