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 )

Metamath Proof Explorer

Theorem umgrunop

Proof