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