Step |
Hyp |
Ref |
Expression |
1 |
|
issubgr.v |
|- V = ( Vtx ` S ) |
2 |
|
issubgr.a |
|- A = ( Vtx ` G ) |
3 |
|
issubgr.i |
|- I = ( iEdg ` S ) |
4 |
|
issubgr.b |
|- B = ( iEdg ` G ) |
5 |
|
issubgr.e |
|- E = ( Edg ` S ) |
6 |
1 2 3 4 5
|
issubgr |
|- ( ( G e. W /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) ) |
7 |
6
|
3adant2 |
|- ( ( G e. W /\ Fun B /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) ) |
8 |
|
resss |
|- ( B |` dom I ) C_ B |
9 |
|
sseq1 |
|- ( I = ( B |` dom I ) -> ( I C_ B <-> ( B |` dom I ) C_ B ) ) |
10 |
8 9
|
mpbiri |
|- ( I = ( B |` dom I ) -> I C_ B ) |
11 |
|
funssres |
|- ( ( Fun B /\ I C_ B ) -> ( B |` dom I ) = I ) |
12 |
11
|
eqcomd |
|- ( ( Fun B /\ I C_ B ) -> I = ( B |` dom I ) ) |
13 |
12
|
ex |
|- ( Fun B -> ( I C_ B -> I = ( B |` dom I ) ) ) |
14 |
13
|
3ad2ant2 |
|- ( ( G e. W /\ Fun B /\ S e. U ) -> ( I C_ B -> I = ( B |` dom I ) ) ) |
15 |
10 14
|
impbid2 |
|- ( ( G e. W /\ Fun B /\ S e. U ) -> ( I = ( B |` dom I ) <-> I C_ B ) ) |
16 |
15
|
3anbi2d |
|- ( ( G e. W /\ Fun B /\ S e. U ) -> ( ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) <-> ( V C_ A /\ I C_ B /\ E C_ ~P V ) ) ) |
17 |
7 16
|
bitrd |
|- ( ( G e. W /\ Fun B /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I C_ B /\ E C_ ~P V ) ) ) |