Metamath Proof Explorer

Theorem upgrun

Description: The union U of two 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, 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=∅
upgrun.u ⊢φ→U∈W
upgrun.v ⊢φ→Vtx⁡U=V
upgrun.un ⊢φ→iEdg⁡U=E∪F
Assertion upgrun ⊢φ→U∈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 upgrun.u ⊢φ→U∈W
9 upgrun.v ⊢φ→Vtx⁡U=V
10 upgrun.un ⊢φ→iEdg⁡U=E∪F
11 5 3 upgrf ⊢G∈UPGraph→E:dom⁡E⟶x∈𝒫V∖∅|x≤2
12 1 11 syl ⊢φ→E:dom⁡E⟶x∈𝒫V∖∅|x≤2
13 eqid ⊢Vtx⁡H=Vtx⁡H
14 13 4 upgrf ⊢H∈UPGraph→F:dom⁡F⟶x∈𝒫Vtx⁡H∖∅|x≤2
15 2 14 syl ⊢φ→F:dom⁡F⟶x∈𝒫Vtx⁡H∖∅|x≤2
16 6 eqcomd ⊢φ→V=Vtx⁡H
17 16 pweqd ⊢φ→𝒫V=𝒫Vtx⁡H
18 17 difeq1d ⊢φ→𝒫V∖∅=𝒫Vtx⁡H∖∅
19 18 rabeqdv ⊢φ→x∈𝒫V∖∅|x≤2=x∈𝒫Vtx⁡H∖∅|x≤2
20 19 feq3d ⊢φ→F:dom⁡F⟶x∈𝒫V∖∅|x≤2↔F:dom⁡F⟶x∈𝒫Vtx⁡H∖∅|x≤2
21 15 20 mpbird ⊢φ→F:dom⁡F⟶x∈𝒫V∖∅|x≤2
22 12 21 7 fun2d ⊢φ→E∪F:dom⁡E∪dom⁡F⟶x∈𝒫V∖∅|x≤2
23 10 dmeqd ⊢φ→dom⁡iEdg⁡U=dom⁡E∪F
24 dmun ⊢dom⁡E∪F=dom⁡E∪dom⁡F
25 23 24 eqtrdi ⊢φ→dom⁡iEdg⁡U=dom⁡E∪dom⁡F
26 9 pweqd ⊢φ→𝒫Vtx⁡U=𝒫V
27 26 difeq1d ⊢φ→𝒫Vtx⁡U∖∅=𝒫V∖∅
28 27 rabeqdv ⊢φ→x∈𝒫Vtx⁡U∖∅|x≤2=x∈𝒫V∖∅|x≤2
29 10 25 28 feq123d ⊢φ→iEdg⁡U:dom⁡iEdg⁡U⟶x∈𝒫Vtx⁡U∖∅|x≤2↔E∪F:dom⁡E∪dom⁡F⟶x∈𝒫V∖∅|x≤2
30 22 29 mpbird ⊢φ→iEdg⁡U:dom⁡iEdg⁡U⟶x∈𝒫Vtx⁡U∖∅|x≤2
31 eqid ⊢Vtx⁡U=Vtx⁡U
32 eqid ⊢iEdg⁡U=iEdg⁡U
33 31 32 isupgr ⊢U∈W→U∈UPGraph↔iEdg⁡U:dom⁡iEdg⁡U⟶x∈𝒫Vtx⁡U∖∅|x≤2
34 8 33 syl ⊢φ→U∈UPGraph↔iEdg⁡U:dom⁡iEdg⁡U⟶x∈𝒫Vtx⁡U∖∅|x≤2
35 30 34 mpbird ⊢φ→U∈UPGraph