Theorem uhgrun

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

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

Proof

Step	Hyp	Ref	Expression
1		uhgrun.g	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
2		uhgrun.h	⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
3		uhgrun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4		uhgrun.f	⊢ 𝐹 = ( iEdg ‘ 𝐻 )
5		uhgrun.vg	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
6		uhgrun.vh	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
7		uhgrun.i	⊢ ( 𝜑 → ( dom 𝐸 ∩ dom 𝐹 ) = ∅ )
8		uhgrun.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
9		uhgrun.v	⊢ ( 𝜑 → ( Vtx ‘ 𝑈 ) = 𝑉 )
10		uhgrun.un	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) = ( 𝐸 ∪ 𝐹 ) )
11	5 3	uhgrf	⊢ ( 𝐺 ∈ UHGraph → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
12	1 11	syl	⊢ ( 𝜑 → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
13		eqid	⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
14	13 4	uhgrf	⊢ ( 𝐻 ∈ UHGraph → 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) )
15	2 14	syl	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) )
16	6	eqcomd	⊢ ( 𝜑 → 𝑉 = ( Vtx ‘ 𝐻 ) )
17	16	pweqd	⊢ ( 𝜑 → 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐻 ) )
18	17	difeq1d	⊢ ( 𝜑 → ( 𝒫 𝑉 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) )
19	18	feq3d	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) ) )
20	15 19	mpbird	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
21	12 20 7	fun2d	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) : ( dom 𝐸 ∪ dom 𝐹 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
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	difeq1d	⊢ ( 𝜑 → ( 𝒫 ( Vtx ‘ 𝑈 ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
27	10 24 26	feq123d	⊢ ( 𝜑 → ( ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑈 ) ∖ { ∅ } ) ↔ ( 𝐸 ∪ 𝐹 ) : ( dom 𝐸 ∪ dom 𝐹 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) )
28	21 27	mpbird	⊢ ( 𝜑 → ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑈 ) ∖ { ∅ } ) )
29		eqid	⊢ ( Vtx ‘ 𝑈 ) = ( Vtx ‘ 𝑈 )
30		eqid	⊢ ( iEdg ‘ 𝑈 ) = ( iEdg ‘ 𝑈 )
31	29 30	isuhgr	⊢ ( 𝑈 ∈ 𝑊 → ( 𝑈 ∈ UHGraph ↔ ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑈 ) ∖ { ∅ } ) ) )
32	8 31	syl	⊢ ( 𝜑 → ( 𝑈 ∈ UHGraph ↔ ( iEdg ‘ 𝑈 ) : dom ( iEdg ‘ 𝑈 ) ⟶ ( 𝒫 ( Vtx ‘ 𝑈 ) ∖ { ∅ } ) ) )
33	28 32	mpbird	⊢ ( 𝜑 → 𝑈 ∈ UHGraph )