Metamath Proof Explorer

Theorem isubgrsubgr

Description: An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025)

Ref Expression
Hypothesis isubgrvtx.v 
|- V = ( Vtx ` G )
Assertion isubgrsubgr 
|- ( ( G e. UHGraph /\ S C_ V ) -> ( G ISubGr S ) SubGraph G )

Proof

Step Hyp Ref Expression
1 isubgrvtx.v 
 |-  V = ( Vtx ` G )
2 1 isubgrvtx 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( Vtx ` ( G ISubGr S ) ) = S )
3 simpr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> S C_ V )
4 2 3 eqsstrd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( Vtx ` ( G ISubGr S ) ) C_ V )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 1 5 isubgriedg 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
7 resss 
 |-  ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ( iEdg ` G )
8 6 7 eqsstrdi 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) C_ ( iEdg ` G ) )
9 simpl 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> G e. UHGraph )
10 5 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
11 10 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> Fun ( iEdg ` G ) )
12 1 isubgruhgr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( G ISubGr S ) e. UHGraph )
13 eqid 
 |-  ( Vtx ` ( G ISubGr S ) ) = ( Vtx ` ( G ISubGr S ) )
14 eqid 
 |-  ( iEdg ` ( G ISubGr S ) ) = ( iEdg ` ( G ISubGr S ) )
15 13 1 14 5 uhgrissubgr 
 |-  ( ( G e. UHGraph /\ Fun ( iEdg ` G ) /\ ( G ISubGr S ) e. UHGraph ) -> ( ( G ISubGr S ) SubGraph G <-> ( ( Vtx ` ( G ISubGr S ) ) C_ V /\ ( iEdg ` ( G ISubGr S ) ) C_ ( iEdg ` G ) ) ) )
16 9 11 12 15 syl3anc 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( G ISubGr S ) SubGraph G <-> ( ( Vtx ` ( G ISubGr S ) ) C_ V /\ ( iEdg ` ( G ISubGr S ) ) C_ ( iEdg ` G ) ) ) )
17 4 8 16 mpbir2and 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( G ISubGr S ) SubGraph G )