egrsubgr

Description: An empty graph consisting of a subset of vertices of a graph (and having no edges) is a subgraph of the graph. (Contributed by AV, 17-Nov-2020) (Proof shortened by AV, 17-Dec-2020)

		Ref	Expression
	Assertion	egrsubgr	$⊢ ((G \in W \land S \in U) \land Vtx (S) \subseteq Vtx (G) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to S SubGraph G$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ ((G \in W \land S \in U) \land Vtx (S) \subseteq Vtx (G) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to Vtx (S) \subseteq Vtx (G)$
2		eqid	$⊢ iEdg (S) = iEdg (S)$
3		eqid	$⊢ Edg (S) = Edg (S)$
4	2 3	edg0iedg0	$⊢ Fun iEdg (S) \to (Edg (S) = \emptyset \leftrightarrow iEdg (S) = \emptyset)$
5	4	adantl	$⊢ ((G \in W \land S \in U) \land Fun iEdg (S)) \to (Edg (S) = \emptyset \leftrightarrow iEdg (S) = \emptyset)$
6		res0	$⊢ {iEdg (G) ↾}_{\emptyset} = \emptyset$
7	6	eqcomi	$⊢ \emptyset = {iEdg (G) ↾}_{\emptyset}$
8		id	$⊢ iEdg (S) = \emptyset \to iEdg (S) = \emptyset$
9		dmeq	$⊢ iEdg (S) = \emptyset \to dom iEdg (S) = dom \emptyset$
10		dm0	$⊢ dom \emptyset = \emptyset$
11	9 10	eqtrdi	$⊢ iEdg (S) = \emptyset \to dom iEdg (S) = \emptyset$
12	11	reseq2d	$⊢ iEdg (S) = \emptyset \to {iEdg (G) ↾}_{dom iEdg (S)} = {iEdg (G) ↾}_{\emptyset}$
13	7 8 12	3eqtr4a	$⊢ iEdg (S) = \emptyset \to iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)}$
14	5 13	biimtrdi	$⊢ ((G \in W \land S \in U) \land Fun iEdg (S)) \to (Edg (S) = \emptyset \to iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)})$
15	14	impr	$⊢ ((G \in W \land S \in U) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)}$
16	15	3adant2	$⊢ ((G \in W \land S \in U) \land Vtx (S) \subseteq Vtx (G) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)}$
17		0ss	$⊢ \emptyset \subseteq 𝒫 Vtx (S)$
18		sseq1	$⊢ Edg (S) = \emptyset \to (Edg (S) \subseteq 𝒫 Vtx (S) \leftrightarrow \emptyset \subseteq 𝒫 Vtx (S))$
19	17 18	mpbiri	$⊢ Edg (S) = \emptyset \to Edg (S) \subseteq 𝒫 Vtx (S)$
20	19	adantl	$⊢ (Fun iEdg (S) \land Edg (S) = \emptyset) \to Edg (S) \subseteq 𝒫 Vtx (S)$
21	20	3ad2ant3	$⊢ ((G \in W \land S \in U) \land Vtx (S) \subseteq Vtx (G) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to Edg (S) \subseteq 𝒫 Vtx (S)$
22		eqid	$⊢ Vtx (S) = Vtx (S)$
23		eqid	$⊢ Vtx (G) = Vtx (G)$
24		eqid	$⊢ iEdg (G) = iEdg (G)$
25	22 23 2 24 3	issubgr	$⊢ (G \in W \land S \in U) \to (S SubGraph G \leftrightarrow (Vtx (S) \subseteq Vtx (G) \land iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)} \land Edg (S) \subseteq 𝒫 Vtx (S)))$
26	25	3ad2ant1	$⊢ ((G \in W \land S \in U) \land Vtx (S) \subseteq Vtx (G) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to (S SubGraph G \leftrightarrow (Vtx (S) \subseteq Vtx (G) \land iEdg (S) = {iEdg (G) ↾}_{dom iEdg (S)} \land Edg (S) \subseteq 𝒫 Vtx (S)))$
27	1 16 21 26	mpbir3and	$⊢ ((G \in W \land S \in U) \land Vtx (S) \subseteq Vtx (G) \land (Fun iEdg (S) \land Edg (S) = \emptyset)) \to S SubGraph G$

Metamath Proof Explorer

Theorem egrsubgr

Proof