Metamath Proof Explorer

Theorem issubgr2

Description: The property of a set to be a subgraph of a set whose edge function is actually a function. (Contributed by AV, 20-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 issubgr2 
|- ( ( G e. W /\ Fun B /\ S e. U ) -> ( S SubGraph G <-> ( V C_ A /\ I C_ B /\ 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 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 ) ) )