Theorem upgrun

Description: The union U of two pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 12-Oct-2020) (Revised by AV, 24-Oct-2021)

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

Proof

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