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