Metamath Proof Explorer


Theorem issubgr

Description: The property of a set to be a subgraph of another set. (Contributed by AV, 16-Nov-2020)

Ref Expression
Hypotheses issubgr.v
|- V = ( Vtx ` S )
issubgr.a
|- A = ( Vtx ` G )
issubgr.i
|- I = ( iEdg ` S )
issubgr.b
|- B = ( iEdg ` G )
issubgr.e
|- E = ( Edg ` S )
Assertion issubgr
|- ( ( G e. W /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ E C_ ~P V ) ) )

Proof

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