This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isuhgrop

Description: The property of being an undirected hypergraph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of Bollobas p. 1. (Contributed by AV, 1-Jan-2020) (Revised by AV, 9-Oct-2020)

Ref Expression
Assertion isuhgrop ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ 𝑉 , 𝐸 ⟩ ∈ V
2 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
3 eqid ⊢ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
4 2 3 isuhgr ⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ V → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ⟶ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ) )
5 1 4 mp1i ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ⟶ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ) )
6 opiedgfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
7 6 dmeqd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = dom 𝐸 )
8 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9 8 pweqd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝒫 𝑉 )
10 9 difeq1d ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
11 6 7 10 feq123d ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ⟶ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
12 5 11 bitrd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )