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 \in W \land Fun B \land S \in U) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I \subseteq B \land E \subseteq 𝒫 V))$

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 \in W \land S \in U) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V))$
7	6	3adant2	$⊢ (G \in W \land Fun B \land S \in U) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V))$
8		resss	$⊢ {B ↾}_{dom I} \subseteq B$
9		sseq1	$⊢ I = {B ↾}_{dom I} \to (I \subseteq B \leftrightarrow {B ↾}_{dom I} \subseteq B)$
10	8 9	mpbiri	$⊢ I = {B ↾}_{dom I} \to I \subseteq B$
11		funssres	$⊢ (Fun B \land I \subseteq B) \to {B ↾}_{dom I} = I$
12	11	eqcomd	$⊢ (Fun B \land I \subseteq B) \to I = {B ↾}_{dom I}$
13	12	ex	$⊢ Fun B \to (I \subseteq B \to I = {B ↾}_{dom I})$
14	13	3ad2ant2	$⊢ (G \in W \land Fun B \land S \in U) \to (I \subseteq B \to I = {B ↾}_{dom I})$
15	10 14	impbid2	$⊢ (G \in W \land Fun B \land S \in U) \to (I = {B ↾}_{dom I} \leftrightarrow I \subseteq B)$
16	15	3anbi2d	$⊢ (G \in W \land Fun B \land S \in U) \to ((V \subseteq A \land I = {B ↾}_{dom I} \land E \subseteq 𝒫 V) \leftrightarrow (V \subseteq A \land I \subseteq B \land E \subseteq 𝒫 V))$
17	7 16	bitrd	$⊢ (G \in W \land Fun B \land S \in U) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I \subseteq B \land E \subseteq 𝒫 V))$

Metamath Proof Explorer