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 |
|
fveq2 |
|- ( s = S -> ( Vtx ` s ) = ( Vtx ` S ) ) |
7 |
6
|
adantr |
|- ( ( s = S /\ g = G ) -> ( Vtx ` s ) = ( Vtx ` S ) ) |
8 |
|
fveq2 |
|- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) ) |
9 |
8
|
adantl |
|- ( ( s = S /\ g = G ) -> ( Vtx ` g ) = ( Vtx ` G ) ) |
10 |
7 9
|
sseq12d |
|- ( ( s = S /\ g = G ) -> ( ( Vtx ` s ) C_ ( Vtx ` g ) <-> ( Vtx ` S ) C_ ( Vtx ` G ) ) ) |
11 |
|
fveq2 |
|- ( s = S -> ( iEdg ` s ) = ( iEdg ` S ) ) |
12 |
11
|
adantr |
|- ( ( s = S /\ g = G ) -> ( iEdg ` s ) = ( iEdg ` S ) ) |
13 |
|
fveq2 |
|- ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) ) |
14 |
13
|
adantl |
|- ( ( s = S /\ g = G ) -> ( iEdg ` g ) = ( iEdg ` G ) ) |
15 |
11
|
dmeqd |
|- ( s = S -> dom ( iEdg ` s ) = dom ( iEdg ` S ) ) |
16 |
15
|
adantr |
|- ( ( s = S /\ g = G ) -> dom ( iEdg ` s ) = dom ( iEdg ` S ) ) |
17 |
14 16
|
reseq12d |
|- ( ( s = S /\ g = G ) -> ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ) |
18 |
12 17
|
eqeq12d |
|- ( ( s = S /\ g = G ) -> ( ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) <-> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ) ) |
19 |
|
fveq2 |
|- ( s = S -> ( Edg ` s ) = ( Edg ` S ) ) |
20 |
6
|
pweqd |
|- ( s = S -> ~P ( Vtx ` s ) = ~P ( Vtx ` S ) ) |
21 |
19 20
|
sseq12d |
|- ( s = S -> ( ( Edg ` s ) C_ ~P ( Vtx ` s ) <-> ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) |
22 |
21
|
adantr |
|- ( ( s = S /\ g = G ) -> ( ( Edg ` s ) C_ ~P ( Vtx ` s ) <-> ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) |
23 |
10 18 22
|
3anbi123d |
|- ( ( s = S /\ g = G ) -> ( ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) <-> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) ) |
24 |
|
df-subgr |
|- SubGraph = { <. s , g >. | ( ( Vtx ` s ) C_ ( Vtx ` g ) /\ ( iEdg ` s ) = ( ( iEdg ` g ) |` dom ( iEdg ` s ) ) /\ ( Edg ` s ) C_ ~P ( Vtx ` s ) ) } |
25 |
23 24
|
brabga |
|- ( ( S e. U /\ G e. W ) -> ( S SubGraph G <-> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) ) |
26 |
25
|
ancoms |
|- ( ( G e. W /\ S e. U ) -> ( S SubGraph G <-> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) ) |
27 |
1 2
|
sseq12i |
|- ( V C_ A <-> ( Vtx ` S ) C_ ( Vtx ` G ) ) |
28 |
3
|
dmeqi |
|- dom I = dom ( iEdg ` S ) |
29 |
4 28
|
reseq12i |
|- ( B |` dom I ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) |
30 |
3 29
|
eqeq12i |
|- ( I = ( B |` dom I ) <-> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ) |
31 |
1
|
pweqi |
|- ~P V = ~P ( Vtx ` S ) |
32 |
5 31
|
sseq12i |
|- ( E C_ ~P V <-> ( Edg ` S ) C_ ~P ( Vtx ` S ) ) |
33 |
27 30 32
|
3anbi123i |
|- ( ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) <-> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) ) |
34 |
26 33
|
bitr4di |
|- ( ( G e. W /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) ) |