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	|- V = ( Vtx ` G )
	isubgriedg.e	|- E = ( iEdg ` G )
Assertion	isubgrvtxuhgr	|- ( G e. UHGraph -> ( G ISubGr V ) = <. V , E >. )

Proof

Step	Hyp	Ref	Expression
1		isubgriedg.v	|- V = ( Vtx ` G )
2		isubgriedg.e	|- E = ( iEdg ` G )
3		ssidd	|- ( G e. UHGraph -> V C_ V )
4	1 2	isisubgr	|- ( ( G e. UHGraph /\ V C_ V ) -> ( G ISubGr V ) = <. V , ( E |` { x e. dom E | ( E ` x ) C_ V } ) >. )
5	3 4	mpdan	|- ( G e. UHGraph -> ( G ISubGr V ) = <. V , ( E |` { x e. dom E | ( E ` x ) C_ V } ) >. )
6	2	uhgrfun	|- ( G e. UHGraph -> Fun E )
7		funrel	|- ( Fun E -> Rel E )
8	6 7	syl	|- ( G e. UHGraph -> Rel E )
9	1 2	uhgrf	|- ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) )
10		ffvelcdm	|- ( ( E : dom E --> ( ~P V \ { (/) } ) /\ x e. dom E ) -> ( E ` x ) e. ( ~P V \ { (/) } ) )
11		eldifi	|- ( ( E ` x ) e. ( ~P V \ { (/) } ) -> ( E ` x ) e. ~P V )
12	11	elpwid	|- ( ( E ` x ) e. ( ~P V \ { (/) } ) -> ( E ` x ) C_ V )
13	10 12	syl	|- ( ( E : dom E --> ( ~P V \ { (/) } ) /\ x e. dom E ) -> ( E ` x ) C_ V )
14	13	rabeqcda	|- ( E : dom E --> ( ~P V \ { (/) } ) -> { x e. dom E | ( E ` x ) C_ V } = dom E )
15	14	eqimsscd	|- ( E : dom E --> ( ~P V \ { (/) } ) -> dom E C_ { x e. dom E | ( E ` x ) C_ V } )
16	9 15	syl	|- ( G e. UHGraph -> dom E C_ { x e. dom E | ( E ` x ) C_ V } )
17		relssres	|- ( ( Rel E /\ dom E C_ { x e. dom E | ( E ` x ) C_ V } ) -> ( E |` { x e. dom E | ( E ` x ) C_ V } ) = E )
18	8 16 17	syl2anc	|- ( G e. UHGraph -> ( E |` { x e. dom E | ( E ` x ) C_ V } ) = E )
19	18	opeq2d	|- ( G e. UHGraph -> <. V , ( E |` { x e. dom E | ( E ` x ) C_ V } ) >. = <. V , E >. )
20	5 19	eqtrd	|- ( G e. UHGraph -> ( G ISubGr V ) = <. V , E >. )