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 ) |