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 )