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