Metamath Proof Explorer

Theorem subusgr

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

Ref Expression
Assertion subusgr 
|- ( ( G e. USGraph /\ S SubGraph G ) -> S e. USGraph )

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 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
8 subgruhgrfun 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
9 7 8 sylan 
 |-  ( ( G e. USGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
10 9 ancoms 
 |-  ( ( S SubGraph G /\ G e. USGraph ) -> Fun ( iEdg ` S ) )
11 10 funfnd 
 |-  ( ( S SubGraph G /\ G e. USGraph ) -> ( 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. USGraph ) ) -> ( 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. USGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> S SubGraph G )
14 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
15 14 adantl 
 |-  ( ( S SubGraph G /\ G e. USGraph ) -> G e. UMGraph )
16 15 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> G e. UMGraph )
17 16 adantr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> G e. UMGraph )
18 simpr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> x e. dom ( iEdg ` S ) )
19 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 } )
20 13 17 18 19 syl3anc 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) e. { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
21 20 ralrimiva 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> A. x e. dom ( iEdg ` S ) ( ( iEdg ` S ) ` x ) e. { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
22 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 } )
23 12 21 22 syl2anc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> ran ( iEdg ` S ) C_ { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
24 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 } ) )
25 12 23 24 sylanbrc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
26 simp2 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( iEdg ` S ) C_ ( iEdg ` G ) )
27 2 4 usgrfs 
 |-  ( G e. USGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { y e. ~P ( Vtx ` G ) | ( # ` y ) = 2 } )
28 df-f1 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { y e. ~P ( Vtx ` G ) | ( # ` y ) = 2 } <-> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { y e. ~P ( Vtx ` G ) | ( # ` y ) = 2 } /\ Fun `' ( iEdg ` G ) ) )
29 ffun 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { y e. ~P ( Vtx ` G ) | ( # ` y ) = 2 } -> Fun ( iEdg ` G ) )
30 29 anim1i 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { y e. ~P ( Vtx ` G ) | ( # ` y ) = 2 } /\ Fun `' ( iEdg ` G ) ) -> ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) ) )
31 28 30 sylbi 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { y e. ~P ( Vtx ` G ) | ( # ` y ) = 2 } -> ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) ) )
32 27 31 syl 
 |-  ( G e. USGraph -> ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) ) )
33 32 adantl 
 |-  ( ( S SubGraph G /\ G e. USGraph ) -> ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) ) )
34 26 33 anim12ci 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> ( ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) )
35 df-3an 
 |-  ( ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) <-> ( ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) )
36 34 35 sylibr 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) )
37 f1ssf1 
 |-  ( ( Fun ( iEdg ` G ) /\ Fun `' ( iEdg ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) ) -> Fun `' ( iEdg ` S ) )
38 36 37 syl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> Fun `' ( iEdg ` S ) )
39 df-f1 
 |-  ( ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } <-> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } /\ Fun `' ( iEdg ` S ) ) )
40 25 38 39 sylanbrc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } )
41 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
42 1 3 isusgrs 
 |-  ( S e. _V -> ( S e. USGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
43 42 adantr 
 |-  ( ( S e. _V /\ G e. _V ) -> ( S e. USGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
44 41 43 syl 
 |-  ( S SubGraph G -> ( S e. USGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
45 44 adantr 
 |-  ( ( S SubGraph G /\ G e. USGraph ) -> ( S e. USGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
46 45 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> ( S e. USGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) -1-1-> { e e. ~P ( Vtx ` S ) | ( # ` e ) = 2 } ) )
47 40 46 mpbird 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. USGraph ) ) -> S e. USGraph )
48 47 ex 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( ( S SubGraph G /\ G e. USGraph ) -> S e. USGraph ) )
49 6 48 syl 
 |-  ( S SubGraph G -> ( ( S SubGraph G /\ G e. USGraph ) -> S e. USGraph ) )
50 49 anabsi8 
 |-  ( ( G e. USGraph /\ S SubGraph G ) -> S e. USGraph )