Metamath Proof Explorer


Theorem uhgrunop

Description: The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are hypergraphs, then <. V , E u. F >. is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 11-Oct-2020) (Revised by AV, 24-Oct-2021)

Ref Expression
Hypotheses uhgrun.g ( 𝜑𝐺 ∈ UHGraph )
uhgrun.h ( 𝜑𝐻 ∈ UHGraph )
uhgrun.e 𝐸 = ( iEdg ‘ 𝐺 )
uhgrun.f 𝐹 = ( iEdg ‘ 𝐻 )
uhgrun.vg 𝑉 = ( Vtx ‘ 𝐺 )
uhgrun.vh ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
uhgrun.i ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
Assertion uhgrunop ( 𝜑 → ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 uhgrun.g ( 𝜑𝐺 ∈ UHGraph )
2 uhgrun.h ( 𝜑𝐻 ∈ UHGraph )
3 uhgrun.e 𝐸 = ( iEdg ‘ 𝐺 )
4 uhgrun.f 𝐹 = ( iEdg ‘ 𝐻 )
5 uhgrun.vg 𝑉 = ( Vtx ‘ 𝐺 )
6 uhgrun.vh ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
7 uhgrun.i ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
8 opex 𝑉 , ( 𝐸𝐹 ) ⟩ ∈ V
9 8 a1i ( 𝜑 → ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ∈ V )
10 5 fvexi 𝑉 ∈ V
11 3 fvexi 𝐸 ∈ V
12 4 fvexi 𝐹 ∈ V
13 11 12 unex ( 𝐸𝐹 ) ∈ V
14 10 13 pm3.2i ( 𝑉 ∈ V ∧ ( 𝐸𝐹 ) ∈ V )
15 opvtxfv ( ( 𝑉 ∈ V ∧ ( 𝐸𝐹 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ) = 𝑉 )
16 14 15 mp1i ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ) = 𝑉 )
17 opiedgfv ( ( 𝑉 ∈ V ∧ ( 𝐸𝐹 ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ) = ( 𝐸𝐹 ) )
18 14 17 mp1i ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ) = ( 𝐸𝐹 ) )
19 1 2 3 4 5 6 7 9 16 18 uhgrun ( 𝜑 → ⟨ 𝑉 , ( 𝐸𝐹 ) ⟩ ∈ UHGraph )