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

Metamath Proof Explorer

Theorem uspgrun

Description: The union U of two simple pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020)

Ref Expression
Hypotheses uspgrun.g ⊢ φ → G ∈ USHGraph
uspgrun.h ⊢ φ → H ∈ USHGraph
uspgrun.e ⊢ E = iEdg ⁡ G
uspgrun.f ⊢ F = iEdg ⁡ H
uspgrun.vg ⊢ V = Vtx ⁡ G
uspgrun.vh ⊢ φ → Vtx ⁡ H = V
uspgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
uspgrun.u ⊢ φ → U ∈ W
uspgrun.v ⊢ φ → Vtx ⁡ U = V
uspgrun.un ⊢ φ → iEdg ⁡ U = E ∪ F
Assertion uspgrun ⊢ φ → U ∈ UPGraph

Proof

Step Hyp Ref Expression
1 uspgrun.g ⊢ φ → G ∈ USHGraph
2 uspgrun.h ⊢ φ → H ∈ USHGraph
3 uspgrun.e ⊢ E = iEdg ⁡ G
4 uspgrun.f ⊢ F = iEdg ⁡ H
5 uspgrun.vg ⊢ V = Vtx ⁡ G
6 uspgrun.vh ⊢ φ → Vtx ⁡ H = V
7 uspgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
8 uspgrun.u ⊢ φ → U ∈ W
9 uspgrun.v ⊢ φ → Vtx ⁡ U = V
10 uspgrun.un ⊢ φ → iEdg ⁡ U = E ∪ F
11 uspgrupgr ⊢ G ∈ USHGraph → G ∈ UPGraph
12 1 11 syl ⊢ φ → G ∈ UPGraph
13 uspgrupgr ⊢ H ∈ USHGraph → H ∈ UPGraph
14 2 13 syl ⊢ φ → H ∈ UPGraph
15 12 14 3 4 5 6 7 8 9 10 upgrun ⊢ φ → U ∈ UPGraph