Theorem isubgrvtxuhgr

Description: The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025)

	Ref	Expression
Hypotheses	isubgriedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isubgriedg.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	isubgrvtxuhgr	⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , 𝐸 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		isubgriedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isubgriedg.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		ssidd	⊢ ( 𝐺 ∈ UHGraph → 𝑉 ⊆ 𝑉 )
4	1 2	isisubgr	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) ⟩ )
5	3 4	mpdan	⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) ⟩ )
6	2	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
7		funrel	⊢ ( Fun 𝐸 → Rel 𝐸 )
8	6 7	syl	⊢ ( 𝐺 ∈ UHGraph → Rel 𝐸 )
9	1 2	uhgrf	⊢ ( 𝐺 ∈ UHGraph → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
10		ffvelcdm	⊢ ( ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 𝑥 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
11		eldifi	⊢ ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝒫 𝑉 )
12	11	elpwid	⊢ ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 )
13	10 12	syl	⊢ ( ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 𝑥 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 )
14	13	rabeqcda	⊢ ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } = dom 𝐸 )
15	14	eqimsscd	⊢ ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → dom 𝐸 ⊆ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } )
16	9 15	syl	⊢ ( 𝐺 ∈ UHGraph → dom 𝐸 ⊆ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } )
17		relssres	⊢ ( ( Rel 𝐸 ∧ dom 𝐸 ⊆ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) → ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) = 𝐸 )
18	8 16 17	syl2anc	⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) = 𝐸 )
19	18	opeq2d	⊢ ( 𝐺 ∈ UHGraph → ⟨ 𝑉 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) ⟩ = ⟨ 𝑉 , 𝐸 ⟩ )
20	5 19	eqtrd	⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , 𝐸 ⟩ )