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	|- ( 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 )