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