isisubgr

Description: The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025)

	Ref	Expression
Hypotheses	isisubgr.v	$⊢ V = Vtx (G)$
	isisubgr.e	$⊢ E = iEdg (G)$
Assertion	isisubgr	$⊢ (G \in W \land S \subseteq V) \to G ISubGr S = ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩$

Proof

Step	Hyp	Ref	Expression
1		isisubgr.v	$⊢ V = Vtx (G)$
2		isisubgr.e	$⊢ E = iEdg (G)$
3		elex	$⊢ G \in W \to G \in V$
4	3	adantr	$⊢ (G \in W \land S \subseteq V) \to G \in V$
5	1	fvexi	$⊢ V \in V$
6	5	a1i	$⊢ S \subseteq V \to V \in V$
7		id	$⊢ S \subseteq V \to S \subseteq V$
8	6 7	sselpwd	$⊢ S \subseteq V \to S \in 𝒫 V$
9	8	adantl	$⊢ (G \in W \land S \subseteq V) \to S \in 𝒫 V$
10		opex	$⊢ ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩ \in V$
11	10	a1i	$⊢ (G \in W \land S \subseteq V) \to ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩ \in V$
12		simpr	$⊢ (g = G \land v = S) \to v = S$
13		fvexd	$⊢ (g = G \land v = S) \to iEdg (g) \in V$
14		fveq2	$⊢ g = G \to iEdg (g) = iEdg (G)$
15	14 2	eqtr4di	$⊢ g = G \to iEdg (g) = E$
16	15	eqeq2d	$⊢ g = G \to (e = iEdg (g) \leftrightarrow e = E)$
17	16	adantr	$⊢ (g = G \land v = S) \to (e = iEdg (g) \leftrightarrow e = E)$
18		simpr	$⊢ (v = S \land e = E) \to e = E$
19		dmeq	$⊢ e = E \to dom e = dom E$
20	19	adantl	$⊢ (v = S \land e = E) \to dom e = dom E$
21		fveq1	$⊢ e = E \to e (x) = E (x)$
22	21	adantl	$⊢ (v = S \land e = E) \to e (x) = E (x)$
23		simpl	$⊢ (v = S \land e = E) \to v = S$
24	22 23	sseq12d	$⊢ (v = S \land e = E) \to (e (x) \subseteq v \leftrightarrow E (x) \subseteq S)$
25	20 24	rabeqbidv	$⊢ (v = S \land e = E) \to \{x \in dom e \| e (x) \subseteq v\} = \{x \in dom E \| E (x) \subseteq S\}$
26	18 25	reseq12d	$⊢ (v = S \land e = E) \to {e ↾}_{\{x \in dom e \| e (x) \subseteq v\}} = {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}$
27	26	ex	$⊢ v = S \to (e = E \to {e ↾}_{\{x \in dom e \| e (x) \subseteq v\}} = {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}})$
28	27	adantl	$⊢ (g = G \land v = S) \to (e = E \to {e ↾}_{\{x \in dom e \| e (x) \subseteq v\}} = {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}})$
29	17 28	sylbid	$⊢ (g = G \land v = S) \to (e = iEdg (g) \to {e ↾}_{\{x \in dom e \| e (x) \subseteq v\}} = {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}})$
30	29	imp	$⊢ ((g = G \land v = S) \land e = iEdg (g)) \to {e ↾}_{\{x \in dom e \| e (x) \subseteq v\}} = {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}$
31	13 30	csbied	$⊢ (g = G \land v = S) \to ⦋ iEdg (g) / e ⦌ ({e ↾}_{\{x \in dom e \| e (x) \subseteq v\}}) = {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}$
32	12 31	opeq12d	$⊢ (g = G \land v = S) \to ⟨v, ⦋ iEdg (g) / e ⦌ ({e ↾}_{\{x \in dom e \| e (x) \subseteq v\}})⟩ = ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩$
33		fveq2	$⊢ g = G \to Vtx (g) = Vtx (G)$
34	33 1	eqtr4di	$⊢ g = G \to Vtx (g) = V$
35	34	pweqd	$⊢ g = G \to 𝒫 Vtx (g) = 𝒫 V$
36		df-isubgr	$⊢ ISubGr = (g \in V, v \in 𝒫 Vtx (g) ⟼ ⟨v, ⦋ iEdg (g) / e ⦌ ({e ↾}_{\{x \in dom e \| e (x) \subseteq v\}})⟩)$
37	32 35 36	ovmpox	$⊢ (G \in V \land S \in 𝒫 V \land ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩ \in V) \to G ISubGr S = ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩$
38	4 9 11 37	syl3anc	$⊢ (G \in W \land S \subseteq V) \to G ISubGr S = ⟨S, {E ↾}_{\{x \in dom E \| E (x) \subseteq S\}}⟩$

Metamath Proof Explorer

Theorem isisubgr

Proof