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