Metamath Proof Explorer

Theorem subuhgr

Description: A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020) (Proof shortened by AV, 21-Nov-2020)

Ref Expression
Assertion subuhgr 
|- ( ( G e. UHGraph /\ S SubGraph G ) -> S e. UHGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 eqid 
 |-  ( Edg ` S ) = ( Edg ` S )
6 1 2 3 4 5 subgrprop2 
 |-  ( S SubGraph G -> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) )
7 subgruhgrfun 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
8 7 ancoms 
 |-  ( ( S SubGraph G /\ G e. UHGraph ) -> Fun ( iEdg ` S ) )
9 8 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> Fun ( iEdg ` S ) )
10 9 funfnd 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> ( iEdg ` S ) Fn dom ( iEdg ` S ) )
11 simplrr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> G e. UHGraph )
12 simplrl 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> S SubGraph G )
13 simpr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> x e. dom ( iEdg ` S ) )
14 1 3 11 12 13 subgruhgredgd 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) e. ( ~P ( Vtx ` S ) \ { (/) } ) )
15 14 ralrimiva 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> A. x e. dom ( iEdg ` S ) ( ( iEdg ` S ) ` x ) e. ( ~P ( Vtx ` S ) \ { (/) } ) )
16 fnfvrnss 
 |-  ( ( ( iEdg ` S ) Fn dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` S ) ( ( iEdg ` S ) ` x ) e. ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ran ( iEdg ` S ) C_ ( ~P ( Vtx ` S ) \ { (/) } ) )
17 10 15 16 syl2anc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> ran ( iEdg ` S ) C_ ( ~P ( Vtx ` S ) \ { (/) } ) )
18 df-f 
 |-  ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) <-> ( ( iEdg ` S ) Fn dom ( iEdg ` S ) /\ ran ( iEdg ` S ) C_ ( ~P ( Vtx ` S ) \ { (/) } ) ) )
19 10 17 18 sylanbrc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) )
20 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
21 1 3 isuhgr 
 |-  ( S e. _V -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
22 21 adantr 
 |-  ( ( S e. _V /\ G e. _V ) -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
23 20 22 syl 
 |-  ( S SubGraph G -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
24 23 adantr 
 |-  ( ( S SubGraph G /\ G e. UHGraph ) -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
25 24 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
26 19 25 mpbird 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UHGraph ) ) -> S e. UHGraph )
27 26 ex 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( ( S SubGraph G /\ G e. UHGraph ) -> S e. UHGraph ) )
28 6 27 syl 
 |-  ( S SubGraph G -> ( ( S SubGraph G /\ G e. UHGraph ) -> S e. UHGraph ) )
29 28 anabsi8 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> S e. UHGraph )