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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrf.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
uhgreq12g.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
uhgreq12g.f ⊢ 𝐹 = ( iEdg ‘ 𝐻 )
Assertion uhgreq12g ( ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) ∧ ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) ) → ( 𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph ) )

Proof

Step Hyp Ref Expression
1 uhgrf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgrf.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 uhgreq12g.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
4 uhgreq12g.f ⊢ 𝐹 = ( iEdg ‘ 𝐻 )
5 1 2 isuhgr ⊢ ( 𝐺 ∈ 𝑋 → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
6 5 adantr ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
7 6 adantr ⊢ ( ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) ∧ ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) ) → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
8 simpr ⊢ ( ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) → 𝐸 = 𝐹 )
9 8 dmeqd ⊢ ( ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) → dom 𝐸 = dom 𝐹 )
10 pweq ⊢ ( 𝑉 = 𝑊 → 𝒫 𝑉 = 𝒫 𝑊 )
11 10 difeq1d ⊢ ( 𝑉 = 𝑊 → ( 𝒫 𝑉 ∖ { ∅ } ) = ( 𝒫 𝑊 ∖ { ∅ } ) )
12 11 adantr ⊢ ( ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) → ( 𝒫 𝑉 ∖ { ∅ } ) = ( 𝒫 𝑊 ∖ { ∅ } ) )
13 8 9 12 feq123d ⊢ ( ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) → ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ 𝐹 : dom 𝐹 ⟶ ( 𝒫 𝑊 ∖ { ∅ } ) ) )
14 3 4 isuhgr ⊢ ( 𝐻 ∈ 𝑌 → ( 𝐻 ∈ UHGraph ↔ 𝐹 : dom 𝐹 ⟶ ( 𝒫 𝑊 ∖ { ∅ } ) ) )
15 14 adantl ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐻 ∈ UHGraph ↔ 𝐹 : dom 𝐹 ⟶ ( 𝒫 𝑊 ∖ { ∅ } ) ) )
16 15 bicomd ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) → ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 𝑊 ∖ { ∅ } ) ↔ 𝐻 ∈ UHGraph ) )
17 13 16 sylan9bbr ⊢ ( ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) ∧ ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) ) → ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ 𝐻 ∈ UHGraph ) )
18 7 17 bitrd ⊢ ( ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ) ∧ ( 𝑉 = 𝑊 ∧ 𝐸 = 𝐹 ) ) → ( 𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph ) )