Theorem umgrun

Description: The union U of two multigraphs G and H with the same vertex set V is a multigraph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 25-Nov-2020)

	Ref	Expression
Hypotheses	umgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
	umgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UMGraph )
	umgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	umgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
	umgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	umgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
	umgrun.i	⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
	umgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	umgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
	umgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
Assertion	umgrun	⊢ ( 𝜑 → 𝑈 ∈ UMGraph )

Proof

Step	Hyp	Ref	Expression
1		umgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UMGraph )
2		umgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UMGraph )
3		umgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4		umgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
5		umgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
6		umgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
7		umgrun.i	⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
8		umgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
9		umgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
10		umgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
11	5 3	umgrf	⊢ ( 𝐺 ∈ UMGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
12	1 11	syl	⊢ ( 𝜑 → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
13		eqid	⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
14	13 4	umgrf	⊢ ( 𝐻 ∈ UMGraph → 𝐹 : dom 𝐹 ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
15	2 14	syl	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
16	6	eqcomd	⊢ ( 𝜑 → 𝑉 = ( Vtx ‘ 𝐻 ) )
17	16	pweqd	⊢ ( 𝜑 → 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐻 ) )
18	17	rabeqdv	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
19	18	feq3d	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐹 : dom 𝐹 ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
20	15 19	mpbird	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
21	12 20 7	fun2d	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) : ( dom 𝐸 ∪ dom 𝐹 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
22	10	dmeqd	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑈 ) = dom ( 𝐸 ∪ 𝐹 ) )
23		dmun	⊢ dom ( 𝐸 ∪ 𝐹 ) = ( dom 𝐸 ∪ dom 𝐹 )
24	22 23	eqtrdi	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑈 ) = ( dom 𝐸 ∪ dom 𝐹 ) )
25	9	pweqd	⊢ ( 𝜑 → 𝒫 ( Vtx ‘ 𝑈 ) = 𝒫 𝑉 )
26	25	rabeqdv	⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝑈 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
27	10 24 26	feq123d	⊢ ( 𝜑 → ( ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝑈 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( 𝐸 ∪ 𝐹 ) : ( dom 𝐸 ∪ dom 𝐹 ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
28	21 27	mpbird	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝑈 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
29		eqid	⊢ ( Vtx ‘ 𝑈 ) = ( Vtx ‘ 𝑈 )
30		eqid	⊢ ( iEdg ‘ 𝑈 ) = ( iEdg ‘ 𝑈 )
31	29 30	isumgrs	⊢ ( 𝑈 ∈ 𝑊 → ( 𝑈 ∈ UMGraph ↔ ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝑈 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
32	8 31	syl	⊢ ( 𝜑 → ( 𝑈 ∈ UMGraph ↔ ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝑈 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
33	28 32	mpbird	⊢ ( 𝜑 → 𝑈 ∈ UMGraph )