This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 >. )