Metamath Proof Explorer

Theorem isubgruhgr

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

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

Proof

Step Hyp Ref Expression
1 isubgrvtx.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 uhgrf 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
4 3 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
5 dmresss 
 |-  dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ dom ( iEdg ` G )
6 5 a1i 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ dom ( iEdg ` G ) )
7 imadmres 
 |-  ( ( iEdg ` G ) " dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) ) = ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } )
8 ffvelcdm 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) /\ y e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` y ) e. ( ~P V \ { (/) } ) )
9 eldifsni 
 |-  ( ( ( iEdg ` G ) ` y ) e. ( ~P V \ { (/) } ) -> ( ( iEdg ` G ) ` y ) =/= (/) )
10 8 9 syl 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) /\ y e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` y ) =/= (/) )
11 10 ex 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) -> ( y e. dom ( iEdg ` G ) -> ( ( iEdg ` G ) ` y ) =/= (/) ) )
12 3 11 syl 
 |-  ( G e. UHGraph -> ( y e. dom ( iEdg ` G ) -> ( ( iEdg ` G ) ` y ) =/= (/) ) )
13 12 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( y e. dom ( iEdg ` G ) -> ( ( iEdg ` G ) ` y ) =/= (/) ) )
14 13 imp 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ y e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` y ) =/= (/) )
15 fvexd 
 |-  ( ( ( iEdg ` G ) ` y ) C_ S -> ( ( iEdg ` G ) ` y ) e. _V )
16 id 
 |-  ( ( ( iEdg ` G ) ` y ) C_ S -> ( ( iEdg ` G ) ` y ) C_ S )
17 15 16 elpwd 
 |-  ( ( ( iEdg ` G ) ` y ) C_ S -> ( ( iEdg ` G ) ` y ) e. ~P S )
18 14 17 anim12ci 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ y e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` G ) ` y ) C_ S ) -> ( ( ( iEdg ` G ) ` y ) e. ~P S /\ ( ( iEdg ` G ) ` y ) =/= (/) ) )
19 eldifsn 
 |-  ( ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) <-> ( ( ( iEdg ` G ) ` y ) e. ~P S /\ ( ( iEdg ` G ) ` y ) =/= (/) ) )
20 18 19 sylibr 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ y e. dom ( iEdg ` G ) ) /\ ( ( iEdg ` G ) ` y ) C_ S ) -> ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) )
21 20 ex 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ y e. dom ( iEdg ` G ) ) -> ( ( ( iEdg ` G ) ` y ) C_ S -> ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) ) )
22 21 ralrimiva 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> A. y e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` y ) C_ S -> ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) ) )
23 fveq2 
 |-  ( x = y -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` y ) )
24 23 sseq1d 
 |-  ( x = y -> ( ( ( iEdg ` G ) ` x ) C_ S <-> ( ( iEdg ` G ) ` y ) C_ S ) )
25 24 ralrab 
 |-  ( A. y e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) <-> A. y e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` y ) C_ S -> ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) ) )
26 22 25 sylibr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> A. y e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) )
27 ffun 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) -> Fun ( iEdg ` G ) )
28 ssrab2 
 |-  { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } C_ dom ( iEdg ` G )
29 27 28 jctir 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) -> ( Fun ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } C_ dom ( iEdg ` G ) ) )
30 3 29 syl 
 |-  ( G e. UHGraph -> ( Fun ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } C_ dom ( iEdg ` G ) ) )
31 30 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( Fun ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } C_ dom ( iEdg ` G ) ) )
32 funimass4 
 |-  ( ( Fun ( iEdg ` G ) /\ { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } C_ dom ( iEdg ` G ) ) -> ( ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ( ~P S \ { (/) } ) <-> A. y e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) ) )
33 31 32 syl 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ( ~P S \ { (/) } ) <-> A. y e. { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ( ( iEdg ` G ) ` y ) e. ( ~P S \ { (/) } ) ) )
34 26 33 mpbird 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( iEdg ` G ) " { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ( ~P S \ { (/) } ) )
35 7 34 eqsstrid 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( iEdg ` G ) " dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) ) C_ ( ~P S \ { (/) } ) )
36 4 6 35 fssrescdmd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( iEdg ` G ) |` dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) ) : dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) --> ( ~P S \ { (/) } ) )
37 resdmres 
 |-  ( ( iEdg ` G ) |` dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) ) = ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } )
38 37 eqcomi 
 |-  ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) = ( ( iEdg ` G ) |` dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
39 38 feq1i 
 |-  ( ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) : dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) --> ( ~P S \ { (/) } ) <-> ( ( iEdg ` G ) |` dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) ) : dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) --> ( ~P S \ { (/) } ) )
40 36 39 sylibr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) : dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) --> ( ~P S \ { (/) } ) )
41 1 2 isubgriedg 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
42 41 dmeqd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> dom ( iEdg ` ( G ISubGr S ) ) = dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
43 1 isubgrvtx 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( Vtx ` ( G ISubGr S ) ) = S )
44 43 pweqd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ~P ( Vtx ` ( G ISubGr S ) ) = ~P S )
45 44 difeq1d 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ~P ( Vtx ` ( G ISubGr S ) ) \ { (/) } ) = ( ~P S \ { (/) } ) )
46 41 42 45 feq123d 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( iEdg ` ( G ISubGr S ) ) : dom ( iEdg ` ( G ISubGr S ) ) --> ( ~P ( Vtx ` ( G ISubGr S ) ) \ { (/) } ) <-> ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) : dom ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) --> ( ~P S \ { (/) } ) ) )
47 40 46 mpbird 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) : dom ( iEdg ` ( G ISubGr S ) ) --> ( ~P ( Vtx ` ( G ISubGr S ) ) \ { (/) } ) )
48 ovexd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( G ISubGr S ) e. _V )
49 eqid 
 |-  ( Vtx ` ( G ISubGr S ) ) = ( Vtx ` ( G ISubGr S ) )
50 eqid 
 |-  ( iEdg ` ( G ISubGr S ) ) = ( iEdg ` ( G ISubGr S ) )
51 49 50 isuhgr 
 |-  ( ( G ISubGr S ) e. _V -> ( ( G ISubGr S ) e. UHGraph <-> ( iEdg ` ( G ISubGr S ) ) : dom ( iEdg ` ( G ISubGr S ) ) --> ( ~P ( Vtx ` ( G ISubGr S ) ) \ { (/) } ) ) )
52 48 51 syl 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( G ISubGr S ) e. UHGraph <-> ( iEdg ` ( G ISubGr S ) ) : dom ( iEdg ` ( G ISubGr S ) ) --> ( ~P ( Vtx ` ( G ISubGr S ) ) \ { (/) } ) ) )
53 47 52 mpbird 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( G ISubGr S ) e. UHGraph )