Theorem umgrunop

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

	Ref	Expression
Hypotheses	umgrun.g	|- ( ph -> G e. UMGraph )
	umgrun.h	|- ( ph -> H e. UMGraph )
	umgrun.e	|- E = ( iEdg ` G )
	umgrun.f	|- F = ( iEdg ` H )
	umgrun.vg	|- V = ( Vtx ` G )
	umgrun.vh	|- ( ph -> ( Vtx ` H ) = V )
	umgrun.i	|- ( ph -> ( dom E i^i dom F ) = (/) )
Assertion	umgrunop	|- ( ph -> <. V , ( E u. F ) >. e. UMGraph )

Proof

Step	Hyp	Ref	Expression
1		umgrun.g	|- ( ph -> G e. UMGraph )
2		umgrun.h	|- ( ph -> H e. UMGraph )
3		umgrun.e	|- E = ( iEdg ` G )
4		umgrun.f	|- F = ( iEdg ` H )
5		umgrun.vg	|- V = ( Vtx ` G )
6		umgrun.vh	|- ( ph -> ( Vtx ` H ) = V )
7		umgrun.i	|- ( ph -> ( dom E i^i dom F ) = (/) )
8		opex	|- <. V , ( E u. F ) >. e. _V
9	8	a1i	|- ( ph -> <. V , ( E u. F ) >. e. _V )
10	5	fvexi	|- V e. _V
11	3	fvexi	|- E e. _V
12	4	fvexi	|- F e. _V
13	11 12	unex	|- ( E u. F ) e. _V
14	10 13	pm3.2i	|- ( V e. _V /\ ( E u. F ) e. _V )
15		opvtxfv	|- ( ( V e. _V /\ ( E u. F ) e. _V ) -> ( Vtx ` <. V , ( E u. F ) >. ) = V )
16	14 15	mp1i	|- ( ph -> ( Vtx ` <. V , ( E u. F ) >. ) = V )
17		opiedgfv	|- ( ( V e. _V /\ ( E u. F ) e. _V ) -> ( iEdg ` <. V , ( E u. F ) >. ) = ( E u. F ) )
18	14 17	mp1i	|- ( ph -> ( iEdg ` <. V , ( E u. F ) >. ) = ( E u. F ) )
19	1 2 3 4 5 6 7 9 16 18	umgrun	|- ( ph -> <. V , ( E u. F ) >. e. UMGraph )