isubgruhgr

Description: An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025)

		Ref	Expression
	Hypothesis	isubgrvtx.v	$⊢ V = Vtx (G)$
	Assertion	isubgruhgr	$⊢ (G \in UHGraph \land S \subseteq V) \to G ISubGr S \in UHGraph$

Proof

Step	Hyp	Ref	Expression
1		isubgrvtx.v	$⊢ V = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	1 2	uhgrf	$⊢ G \in UHGraph \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
4	3	adantr	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
5		dmresss	$⊢ dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) \subseteq dom iEdg (G)$
6	5	a1i	$⊢ (G \in UHGraph \land S \subseteq V) \to dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) \subseteq dom iEdg (G)$
7		imadmres	$⊢ iEdg (G) [dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})] = iEdg (G) [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}]$
8		ffvelcdm	$⊢ (iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \land y \in dom iEdg (G)) \to iEdg (G) (y) \in (𝒫 V ∖ \{\emptyset\})$
9		eldifsni	$⊢ iEdg (G) (y) \in (𝒫 V ∖ \{\emptyset\}) \to iEdg (G) (y) \neq \emptyset$
10	8 9	syl	$⊢ (iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \land y \in dom iEdg (G)) \to iEdg (G) (y) \neq \emptyset$
11	10	ex	$⊢ iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \to (y \in dom iEdg (G) \to iEdg (G) (y) \neq \emptyset)$
12	3 11	syl	$⊢ G \in UHGraph \to (y \in dom iEdg (G) \to iEdg (G) (y) \neq \emptyset)$
13	12	adantr	$⊢ (G \in UHGraph \land S \subseteq V) \to (y \in dom iEdg (G) \to iEdg (G) (y) \neq \emptyset)$
14	13	imp	$⊢ ((G \in UHGraph \land S \subseteq V) \land y \in dom iEdg (G)) \to iEdg (G) (y) \neq \emptyset$
15		fvexd	$⊢ iEdg (G) (y) \subseteq S \to iEdg (G) (y) \in V$
16		id	$⊢ iEdg (G) (y) \subseteq S \to iEdg (G) (y) \subseteq S$
17	15 16	elpwd	$⊢ iEdg (G) (y) \subseteq S \to iEdg (G) (y) \in 𝒫 S$
18	14 17	anim12ci	$⊢ (((G \in UHGraph \land S \subseteq V) \land y \in dom iEdg (G)) \land iEdg (G) (y) \subseteq S) \to (iEdg (G) (y) \in 𝒫 S \land iEdg (G) (y) \neq \emptyset)$
19		eldifsn	$⊢ iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}) \leftrightarrow (iEdg (G) (y) \in 𝒫 S \land iEdg (G) (y) \neq \emptyset)$
20	18 19	sylibr	$⊢ (((G \in UHGraph \land S \subseteq V) \land y \in dom iEdg (G)) \land iEdg (G) (y) \subseteq S) \to iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\})$
21	20	ex	$⊢ ((G \in UHGraph \land S \subseteq V) \land y \in dom iEdg (G)) \to (iEdg (G) (y) \subseteq S \to iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}))$
22	21	ralrimiva	$⊢ (G \in UHGraph \land S \subseteq V) \to \forall y \in dom iEdg (G) (iEdg (G) (y) \subseteq S \to iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}))$
23		fveq2	$⊢ x = y \to iEdg (G) (x) = iEdg (G) (y)$
24	23	sseq1d	$⊢ x = y \to (iEdg (G) (x) \subseteq S \leftrightarrow iEdg (G) (y) \subseteq S)$
25	24	ralrab	$⊢ \forall y \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}) \leftrightarrow \forall y \in dom iEdg (G) (iEdg (G) (y) \subseteq S \to iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}))$
26	22 25	sylibr	$⊢ (G \in UHGraph \land S \subseteq V) \to \forall y \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\})$
27		ffun	$⊢ iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \to Fun iEdg (G)$
28		ssrab2	$⊢ \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} \subseteq dom iEdg (G)$
29	27 28	jctir	$⊢ iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\} \to (Fun iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} \subseteq dom iEdg (G))$
30	3 29	syl	$⊢ G \in UHGraph \to (Fun iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} \subseteq dom iEdg (G))$
31	30	adantr	$⊢ (G \in UHGraph \land S \subseteq V) \to (Fun iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} \subseteq dom iEdg (G))$
32		funimass4	$⊢ (Fun iEdg (G) \land \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} \subseteq dom iEdg (G)) \to (iEdg (G) [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}] \subseteq 𝒫 S ∖ \{\emptyset\} \leftrightarrow \forall y \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}))$
33	31 32	syl	$⊢ (G \in UHGraph \land S \subseteq V) \to (iEdg (G) [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}] \subseteq 𝒫 S ∖ \{\emptyset\} \leftrightarrow \forall y \in \{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\} iEdg (G) (y) \in (𝒫 S ∖ \{\emptyset\}))$
34	26 33	mpbird	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G) [\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}] \subseteq 𝒫 S ∖ \{\emptyset\}$
35	7 34	eqsstrid	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G) [dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})] \subseteq 𝒫 S ∖ \{\emptyset\}$
36	4 6 35	fssrescdmd	$⊢ (G \in UHGraph \land S \subseteq V) \to ({iEdg (G) ↾}_{dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})}) : dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) ⟶ 𝒫 S ∖ \{\emptyset\}$
37		resdmres	$⊢ {iEdg (G) ↾}_{dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})} = {iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}$
38	37	eqcomi	$⊢ {iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}} = {iEdg (G) ↾}_{dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})}$
39	38	feq1i	$⊢ ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) : dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) ⟶ 𝒫 S ∖ \{\emptyset\} \leftrightarrow ({iEdg (G) ↾}_{dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})}) : dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) ⟶ 𝒫 S ∖ \{\emptyset\}$
40	36 39	sylibr	$⊢ (G \in UHGraph \land S \subseteq V) \to ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) : dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) ⟶ 𝒫 S ∖ \{\emptyset\}$
41	1 2	isubgriedg	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G ISubGr S) = {iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}$
42	41	dmeqd	$⊢ (G \in UHGraph \land S \subseteq V) \to dom iEdg (G ISubGr S) = dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}})$
43	1	isubgrvtx	$⊢ (G \in UHGraph \land S \subseteq V) \to Vtx (G ISubGr S) = S$
44	43	pweqd	$⊢ (G \in UHGraph \land S \subseteq V) \to 𝒫 Vtx (G ISubGr S) = 𝒫 S$
45	44	difeq1d	$⊢ (G \in UHGraph \land S \subseteq V) \to 𝒫 Vtx (G ISubGr S) ∖ \{\emptyset\} = 𝒫 S ∖ \{\emptyset\}$
46	41 42 45	feq123d	$⊢ (G \in UHGraph \land S \subseteq V) \to (iEdg (G ISubGr S) : dom iEdg (G ISubGr S) ⟶ 𝒫 Vtx (G ISubGr S) ∖ \{\emptyset\} \leftrightarrow ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) : dom ({iEdg (G) ↾}_{\{x \in dom iEdg (G) \| iEdg (G) (x) \subseteq S\}}) ⟶ 𝒫 S ∖ \{\emptyset\})$
47	40 46	mpbird	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G ISubGr S) : dom iEdg (G ISubGr S) ⟶ 𝒫 Vtx (G ISubGr S) ∖ \{\emptyset\}$
48		ovexd	$⊢ (G \in UHGraph \land S \subseteq V) \to G ISubGr S \in V$
49		eqid	$⊢ Vtx (G ISubGr S) = Vtx (G ISubGr S)$
50		eqid	$⊢ iEdg (G ISubGr S) = iEdg (G ISubGr S)$
51	49 50	isuhgr	$⊢ G ISubGr S \in V \to (G ISubGr S \in UHGraph \leftrightarrow iEdg (G ISubGr S) : dom iEdg (G ISubGr S) ⟶ 𝒫 Vtx (G ISubGr S) ∖ \{\emptyset\})$
52	48 51	syl	$⊢ (G \in UHGraph \land S \subseteq V) \to (G ISubGr S \in UHGraph \leftrightarrow iEdg (G ISubGr S) : dom iEdg (G ISubGr S) ⟶ 𝒫 Vtx (G ISubGr S) ∖ \{\emptyset\})$
53	47 52	mpbird	$⊢ (G \in UHGraph \land S \subseteq V) \to G ISubGr S \in UHGraph$

Metamath Proof Explorer

Theorem isubgruhgr

Proof