Metamath Proof Explorer

Theorem subupgr

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

Ref Expression
Assertion subupgr 
|- ( ( G e. UPGraph /\ S SubGraph G ) -> S e. UPGraph )

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 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
8 subgruhgrfun 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
9 7 8 sylan 
 |-  ( ( G e. UPGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
10 9 ancoms 
 |-  ( ( S SubGraph G /\ G e. UPGraph ) -> Fun ( iEdg ` S ) )
11 10 funfnd 
 |-  ( ( S SubGraph G /\ G e. UPGraph ) -> ( 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. UPGraph ) ) -> ( iEdg ` S ) Fn dom ( iEdg ` S ) )
13 fveq2 
 |-  ( e = ( ( iEdg ` S ) ` x ) -> ( # ` e ) = ( # ` ( ( iEdg ` S ) ` x ) ) )
14 13 breq1d 
 |-  ( e = ( ( iEdg ` S ) ` x ) -> ( ( # ` e ) <_ 2 <-> ( # ` ( ( iEdg ` S ) ` x ) ) <_ 2 ) )
15 7 anim2i 
 |-  ( ( S SubGraph G /\ G e. UPGraph ) -> ( S SubGraph G /\ G e. UHGraph ) )
16 15 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( S SubGraph G /\ G e. UHGraph ) )
17 16 ancomd 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( G e. UHGraph /\ S SubGraph G ) )
18 17 anim1i 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( G e. UHGraph /\ S SubGraph G ) /\ x e. dom ( iEdg ` S ) ) )
19 18 simplld 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> G e. UHGraph )
20 simpl 
 |-  ( ( S SubGraph G /\ G e. UPGraph ) -> S SubGraph G )
21 20 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> S SubGraph G )
22 21 adantr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> S SubGraph G )
23 simpr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> x e. dom ( iEdg ` S ) )
24 1 3 19 22 23 subgruhgredgd 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) e. ( ~P ( Vtx ` S ) \ { (/) } ) )
25 4 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
26 7 25 syl 
 |-  ( G e. UPGraph -> Fun ( iEdg ` G ) )
27 26 ad2antll 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> Fun ( iEdg ` G ) )
28 27 adantr 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> Fun ( iEdg ` G ) )
29 simpll2 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( iEdg ` S ) C_ ( iEdg ` G ) )
30 funssfv 
 |-  ( ( Fun ( iEdg ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` S ) ` x ) )
31 28 29 23 30 syl3anc 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` S ) ` x ) )
32 31 eqcomd 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) = ( ( iEdg ` G ) ` x ) )
33 32 fveq2d 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( # ` ( ( iEdg ` S ) ` x ) ) = ( # ` ( ( iEdg ` G ) ` x ) ) )
34 subgreldmiedg 
 |-  ( ( S SubGraph G /\ x e. dom ( iEdg ` S ) ) -> x e. dom ( iEdg ` G ) )
35 34 ex 
 |-  ( S SubGraph G -> ( x e. dom ( iEdg ` S ) -> x e. dom ( iEdg ` G ) ) )
36 35 adantr 
 |-  ( ( S SubGraph G /\ G e. UPGraph ) -> ( x e. dom ( iEdg ` S ) -> x e. dom ( iEdg ` G ) ) )
37 36 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( x e. dom ( iEdg ` S ) -> x e. dom ( iEdg ` G ) ) )
38 simpr 
 |-  ( ( x e. dom ( iEdg ` G ) /\ G e. UPGraph ) -> G e. UPGraph )
39 26 funfnd 
 |-  ( G e. UPGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
40 39 adantl 
 |-  ( ( x e. dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
41 simpl 
 |-  ( ( x e. dom ( iEdg ` G ) /\ G e. UPGraph ) -> x e. dom ( iEdg ` G ) )
42 2 4 upgrle 
 |-  ( ( G e. UPGraph /\ ( iEdg ` G ) Fn dom ( iEdg ` G ) /\ x e. dom ( iEdg ` G ) ) -> ( # ` ( ( iEdg ` G ) ` x ) ) <_ 2 )
43 38 40 41 42 syl3anc 
 |-  ( ( x e. dom ( iEdg ` G ) /\ G e. UPGraph ) -> ( # ` ( ( iEdg ` G ) ` x ) ) <_ 2 )
44 43 expcom 
 |-  ( G e. UPGraph -> ( x e. dom ( iEdg ` G ) -> ( # ` ( ( iEdg ` G ) ` x ) ) <_ 2 ) )
45 44 ad2antll 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( x e. dom ( iEdg ` G ) -> ( # ` ( ( iEdg ` G ) ` x ) ) <_ 2 ) )
46 37 45 syld 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( x e. dom ( iEdg ` S ) -> ( # ` ( ( iEdg ` G ) ` x ) ) <_ 2 ) )
47 46 imp 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( # ` ( ( iEdg ` G ) ` x ) ) <_ 2 )
48 33 47 eqbrtrd 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( # ` ( ( iEdg ` S ) ` x ) ) <_ 2 )
49 14 24 48 elrabd 
 |-  ( ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) /\ x e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` x ) e. { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } )
50 49 ralrimiva 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> A. x e. dom ( iEdg ` S ) ( ( iEdg ` S ) ` x ) e. { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } )
51 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 } )
52 12 50 51 syl2anc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ran ( iEdg ` S ) C_ { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } )
53 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 } ) )
54 12 52 53 sylanbrc 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } )
55 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
56 1 3 isupgr 
 |-  ( S e. _V -> ( S e. UPGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } ) )
57 56 adantr 
 |-  ( ( S e. _V /\ G e. _V ) -> ( S e. UPGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } ) )
58 55 57 syl 
 |-  ( S SubGraph G -> ( S e. UPGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } ) )
59 58 adantr 
 |-  ( ( S SubGraph G /\ G e. UPGraph ) -> ( S e. UPGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } ) )
60 59 adantl 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> ( S e. UPGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> { e e. ( ~P ( Vtx ` S ) \ { (/) } ) | ( # ` e ) <_ 2 } ) )
61 54 60 mpbird 
 |-  ( ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) /\ ( S SubGraph G /\ G e. UPGraph ) ) -> S e. UPGraph )
62 61 ex 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( ( S SubGraph G /\ G e. UPGraph ) -> S e. UPGraph ) )
63 6 62 syl 
 |-  ( S SubGraph G -> ( ( S SubGraph G /\ G e. UPGraph ) -> S e. UPGraph ) )
64 63 anabsi8 
 |-  ( ( G e. UPGraph /\ S SubGraph G ) -> S e. UPGraph )