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 W Fun B S U S SubGraph G V A I B E 𝒫 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 W S U S SubGraph G V A I = B dom I E 𝒫 V
7 6 3adant2 G W Fun B S U S SubGraph G V A I = B dom I E 𝒫 V
8 resss B dom I B
9 sseq1 I = B dom I I B B dom I B
10 8 9 mpbiri I = B dom I I B
11 funssres Fun B I B B dom I = I
12 11 eqcomd Fun B I B I = B dom I
13 12 ex Fun B I B I = B dom I
14 13 3ad2ant2 G W Fun B S U I B I = B dom I
15 10 14 impbid2 G W Fun B S U I = B dom I I B
16 15 3anbi2d G W Fun B S U V A I = B dom I E 𝒫 V V A I B E 𝒫 V
17 7 16 bitrd G W Fun B S U S SubGraph G V A I B E 𝒫 V