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	\|- ( ph -> G e. UPGraph )
	upgrun.h	\|- ( ph -> H e. UPGraph )
	upgrun.e	\|- E = ( iEdg ` G )
	upgrun.f	\|- F = ( iEdg ` H )
	upgrun.vg	\|- V = ( Vtx ` G )
	upgrun.vh	\|- ( ph -> ( Vtx ` H ) = V )
	upgrun.i	\|- ( ph -> ( dom E i^i dom F ) = (/) )
Assertion	upgrunop	\|- ( ph -> <. V , ( E u. F ) >. e. UPGraph )

Proof

Step	Hyp	Ref	Expression
1		upgrun.g	\|- ( ph -> G e. UPGraph )
2		upgrun.h	\|- ( ph -> H e. UPGraph )
3		upgrun.e	\|- E = ( iEdg ` G )
4		upgrun.f	\|- F = ( iEdg ` H )
5		upgrun.vg	\|- V = ( Vtx ` G )
6		upgrun.vh	\|- ( ph -> ( Vtx ` H ) = V )
7		upgrun.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	upgrun	\|- ( ph -> <. V , ( E u. F ) >. e. UPGraph )

Metamath Proof Explorer

Theorem upgrunop

Proof