Metamath Proof Explorer

Theorem subumgr

Description: A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020)

Ref Expression
Assertion subumgr 
|- ( ( G e. UMGraph /\ S SubGraph G ) -> S e. UMGraph )

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 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
8 subgruhgrfun 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
9 7 8 sylan 
 |-  ( ( G e. UMGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
10 9 ancoms 
 |-  ( ( S SubGraph G /\ G e. UMGraph ) -> Fun ( iEdg ` S ) )
11 10 funfnd 
 |-  ( ( S SubGraph G /\ G e. UMGraph ) -> ( iEdg ` S ) Fn dom ( iEdg ` S ) )
12 11 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) -> ( iEdg ` S ) Fn dom ( iEdg ` S ) )
13 simplrl 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> S SubGraph G )
14 simplrr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> G e. UMGraph )
15 simpr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> x e. dom ( iEdg ` S ) )
16 1 3 subumgredg2 
 |-  ( ( S SubGraph G /\ G e. UMGraph /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) e. { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
17 13 14 15 16 syl3anc 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) e. { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
18 17 ralrimiva 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) -> A. x e. dom ( iEdg ` S ) ( ( iEdg ` S ) ` x ) e. { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
19 fnfvrnss 
 |-  ( ( ( iEdg ` S ) Fn dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` S ) ( ( iEdg ` S ) ` x ) e. { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) -> ran ( iEdg ` S ) C_ { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
20 12 18 19 syl2anc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) -> ran ( iEdg ` S ) C_ { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
21 df-f 
 |-  ( ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } <-> ( ( iEdg ` S ) Fn dom ( iEdg ` S ) /\ ran ( iEdg ` S ) C_ { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
22 12 20 21 sylanbrc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) -> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
23 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
24 1 3 isumgrs 
 |-  ( S e. _V -> ( S e. UMGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
25 24 adantr 
 |-  ( ( S e. _V /\ G e. _V ) -> ( S e. UMGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
26 23 25 syl 
 |-  ( S SubGraph G -> ( S e. UMGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
27 26 ad2antrl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) -> ( S e. UMGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
28 22 27 mpbird 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UMGraph ) ) -> S e. UMGraph )
29 28 ex 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( ( S SubGraph G /\ G e. UMGraph ) -> S e. UMGraph ) )
30 6 29 syl 
 |-  ( S SubGraph G -> ( ( S SubGraph G /\ G e. UMGraph ) -> S e. UMGraph ) )
31 30 anabsi8 
 |-  ( ( G e. UMGraph /\ S SubGraph G ) -> S e. UMGraph )