Metamath Proof Explorer

Theorem upgrunop

Description: The union of two pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 12-Oct-2020) (Revised by AV, 24-Oct-2021)

Ref Expression
Hypotheses upgrun.g ⊢ φ → G ∈ UPGraph
upgrun.h ⊢ φ → H ∈ UPGraph
upgrun.e ⊢ E = iEdg ⁡ G
upgrun.f ⊢ F = iEdg ⁡ H
upgrun.vg ⊢ V = Vtx ⁡ G
upgrun.vh ⊢ φ → Vtx ⁡ H = V
upgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
Assertion upgrunop ⊢ φ → V E ∪ F ∈ UPGraph

Proof

Step Hyp Ref Expression
1 upgrun.g ⊢ φ → G ∈ UPGraph
2 upgrun.h ⊢ φ → H ∈ UPGraph
3 upgrun.e ⊢ E = iEdg ⁡ G
4 upgrun.f ⊢ F = iEdg ⁡ H
5 upgrun.vg ⊢ V = Vtx ⁡ G
6 upgrun.vh ⊢ φ → Vtx ⁡ H = V
7 upgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
8 opex ⊢ V E ∪ F ∈ V
9 8 a1i ⊢ φ → V E ∪ F ∈ V
10 5 fvexi ⊢ V ∈ V
11 3 fvexi ⊢ E ∈ V
12 4 fvexi ⊢ F ∈ V
13 11 12 unex ⊢ E ∪ F ∈ V
14 10 13 pm3.2i ⊢ V ∈ V ∧ E ∪ F ∈ V
15 opvtxfv ⊢ V ∈ V ∧ E ∪ F ∈ V → Vtx ⁡ V E ∪ F = V
16 14 15 mp1i ⊢ φ → Vtx ⁡ V E ∪ F = V
17 opiedgfv ⊢ V ∈ V ∧ E ∪ F ∈ V → iEdg ⁡ V E ∪ F = E ∪ F
18 14 17 mp1i ⊢ φ → iEdg ⁡ V E ∪ F = E ∪ F
19 1 2 3 4 5 6 7 9 16 18 upgrun ⊢ φ → V E ∪ F ∈ UPGraph