isubgredg

Description: An edge of an induced subgraph of a hypergraph is an edge of the hypergraph connecting vertices of the subgraph. (Contributed by AV, 24-Sep-2025)

	Ref	Expression
Hypotheses	isubgredg.v	$⊢ V = Vtx (G)$
	isubgredg.e	$⊢ E = Edg (G)$
	isubgredg.h	$⊢ H = G ISubGr S$
	isubgredg.i	$⊢ I = Edg (H)$
Assertion	isubgredg	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in I \leftrightarrow (K \in E \land K \subseteq S))$

Proof

Step	Hyp	Ref	Expression
1		isubgredg.v	$⊢ V = Vtx (G)$
2		isubgredg.e	$⊢ E = Edg (G)$
3		isubgredg.h	$⊢ H = G ISubGr S$
4		isubgredg.i	$⊢ I = Edg (H)$
5	3	fveq2i	$⊢ iEdg (H) = iEdg (G ISubGr S)$
6		eqid	$⊢ iEdg (G) = iEdg (G)$
7	1 6	isubgriedg	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G ISubGr S) = {iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}$
8	5 7	eqtrid	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (H) = {iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}$
9	8	rneqd	$⊢ (G \in UHGraph \land S \subseteq V) \to ran iEdg (H) = ran ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}})$
10	9	eleq2d	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in ran iEdg (H) \leftrightarrow K \in ran ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}))$
11	1 6	uhgrf	$⊢ G \in UHGraph \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
12	11	adantr	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G) : dom iEdg (G) ⟶ 𝒫 V ∖ \{\emptyset\}$
13	12	ffnd	$⊢ (G \in UHGraph \land S \subseteq V) \to iEdg (G) Fn dom iEdg (G)$
14		ssrab2	$⊢ \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \subseteq dom iEdg (G)$
15	14	a1i	$⊢ (G \in UHGraph \land S \subseteq V) \to \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \subseteq dom iEdg (G)$
16	13 15	fnssresd	$⊢ (G \in UHGraph \land S \subseteq V) \to ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) Fn \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}$
17		fvelrnb	$⊢ ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) Fn \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \to (K \in ran ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) \leftrightarrow \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
18	16 17	syl	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in ran ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) \leftrightarrow \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
19		fvres	$⊢ x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \to ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = iEdg (G) (x)$
20	19	adantl	$⊢ ((G \in UHGraph \land S \subseteq V) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = iEdg (G) (x)$
21	20	eqeq1d	$⊢ ((G \in UHGraph \land S \subseteq V) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to (({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K \leftrightarrow iEdg (G) (x) = K)$
22		fveq2	$⊢ i = x \to iEdg (G) (i) = iEdg (G) (x)$
23	22	sseq1d	$⊢ i = x \to (iEdg (G) (i) \subseteq S \leftrightarrow iEdg (G) (x) \subseteq S)$
24	23	elrab	$⊢ x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \leftrightarrow (x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S)$
25	6	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
26	25	adantr	$⊢ (G \in UHGraph \land S \subseteq V) \to Fun iEdg (G)$
27		simpl	$⊢ (x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S) \to x \in dom iEdg (G)$
28		fvelrn	$⊢ (Fun iEdg (G) \land x \in dom iEdg (G)) \to iEdg (G) (x) \in ran iEdg (G)$
29	26 27 28	syl2anr	$⊢ ((x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S) \land (G \in UHGraph \land S \subseteq V)) \to iEdg (G) (x) \in ran iEdg (G)$
30		simpr	$⊢ (x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S) \to iEdg (G) (x) \subseteq S$
31	30	adantr	$⊢ ((x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S) \land (G \in UHGraph \land S \subseteq V)) \to iEdg (G) (x) \subseteq S$
32	29 31	jca	$⊢ ((x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S) \land (G \in UHGraph \land S \subseteq V)) \to (iEdg (G) (x) \in ran iEdg (G) \land iEdg (G) (x) \subseteq S)$
33	32	ex	$⊢ (x \in dom iEdg (G) \land iEdg (G) (x) \subseteq S) \to ((G \in UHGraph \land S \subseteq V) \to (iEdg (G) (x) \in ran iEdg (G) \land iEdg (G) (x) \subseteq S))$
34	24 33	sylbi	$⊢ x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \to ((G \in UHGraph \land S \subseteq V) \to (iEdg (G) (x) \in ran iEdg (G) \land iEdg (G) (x) \subseteq S))$
35	34	impcom	$⊢ ((G \in UHGraph \land S \subseteq V) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to (iEdg (G) (x) \in ran iEdg (G) \land iEdg (G) (x) \subseteq S)$
36		eleq1	$⊢ iEdg (G) (x) = K \to (iEdg (G) (x) \in ran iEdg (G) \leftrightarrow K \in ran iEdg (G))$
37		sseq1	$⊢ iEdg (G) (x) = K \to (iEdg (G) (x) \subseteq S \leftrightarrow K \subseteq S)$
38	36 37	anbi12d	$⊢ iEdg (G) (x) = K \to ((iEdg (G) (x) \in ran iEdg (G) \land iEdg (G) (x) \subseteq S) \leftrightarrow (K \in ran iEdg (G) \land K \subseteq S))$
39	35 38	syl5ibcom	$⊢ ((G \in UHGraph \land S \subseteq V) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to (iEdg (G) (x) = K \to (K \in ran iEdg (G) \land K \subseteq S))$
40	21 39	sylbid	$⊢ ((G \in UHGraph \land S \subseteq V) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to (({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K \to (K \in ran iEdg (G) \land K \subseteq S))$
41	40	rexlimdva	$⊢ (G \in UHGraph \land S \subseteq V) \to (\exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K \to (K \in ran iEdg (G) \land K \subseteq S))$
42		edgval	$⊢ Edg (G) = ran iEdg (G)$
43	42	eqcomi	$⊢ ran iEdg (G) = Edg (G)$
44	43	eleq2i	$⊢ K \in ran iEdg (G) \leftrightarrow K \in Edg (G)$
45	6	edgiedgb	$⊢ Fun iEdg (G) \to (K \in Edg (G) \leftrightarrow \exists x \in dom iEdg (G) K = iEdg (G) (x))$
46	44 45	bitrid	$⊢ Fun iEdg (G) \to (K \in ran iEdg (G) \leftrightarrow \exists x \in dom iEdg (G) K = iEdg (G) (x))$
47	25 46	syl	$⊢ G \in UHGraph \to (K \in ran iEdg (G) \leftrightarrow \exists x \in dom iEdg (G) K = iEdg (G) (x))$
48	47	adantr	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in ran iEdg (G) \leftrightarrow \exists x \in dom iEdg (G) K = iEdg (G) (x))$
49		simprl	$⊢ (((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \to x \in dom iEdg (G)$
50		simpr	$⊢ (x \in dom iEdg (G) \land K = iEdg (G) (x)) \to K = iEdg (G) (x)$
51	50	sseq1d	$⊢ (x \in dom iEdg (G) \land K = iEdg (G) (x)) \to (K \subseteq S \leftrightarrow iEdg (G) (x) \subseteq S)$
52	51	biimpcd	$⊢ K \subseteq S \to ((x \in dom iEdg (G) \land K = iEdg (G) (x)) \to iEdg (G) (x) \subseteq S)$
53	52	adantl	$⊢ ((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \to ((x \in dom iEdg (G) \land K = iEdg (G) (x)) \to iEdg (G) (x) \subseteq S)$
54	53	imp	$⊢ (((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \to iEdg (G) (x) \subseteq S$
55	49 54 24	sylanbrc	$⊢ (((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \to x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}$
56		simpr	$⊢ ((((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}$
57	50	eqcomd	$⊢ (x \in dom iEdg (G) \land K = iEdg (G) (x)) \to iEdg (G) (x) = K$
58	57	adantl	$⊢ (((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \to iEdg (G) (x) = K$
59	19 58	sylan9eqr	$⊢ ((((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K$
60	56 59	jca	$⊢ ((((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \land x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}) \to (x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \land ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
61	55 60	mpdan	$⊢ (((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \land (x \in dom iEdg (G) \land K = iEdg (G) (x))) \to (x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \land ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
62	61	ex	$⊢ ((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \to ((x \in dom iEdg (G) \land K = iEdg (G) (x)) \to (x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \land ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K))$
63	62	eximdv	$⊢ ((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \to (\exists x (x \in dom iEdg (G) \land K = iEdg (G) (x)) \to \exists x (x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \land ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K))$
64		df-rex	$⊢ \exists x \in dom iEdg (G) K = iEdg (G) (x) \leftrightarrow \exists x (x \in dom iEdg (G) \land K = iEdg (G) (x))$
65		df-rex	$⊢ \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K \leftrightarrow \exists x (x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} \land ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
66	63 64 65	3imtr4g	$⊢ ((G \in UHGraph \land S \subseteq V) \land K \subseteq S) \to (\exists x \in dom iEdg (G) K = iEdg (G) (x) \to \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
67	66	ex	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \subseteq S \to (\exists x \in dom iEdg (G) K = iEdg (G) (x) \to \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K))$
68	67	com23	$⊢ (G \in UHGraph \land S \subseteq V) \to (\exists x \in dom iEdg (G) K = iEdg (G) (x) \to (K \subseteq S \to \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K))$
69	48 68	sylbid	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in ran iEdg (G) \to (K \subseteq S \to \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K))$
70	69	impd	$⊢ (G \in UHGraph \land S \subseteq V) \to ((K \in ran iEdg (G) \land K \subseteq S) \to \exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K)$
71	41 70	impbid	$⊢ (G \in UHGraph \land S \subseteq V) \to (\exists x \in \{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\} ({iEdg (G) ↾}_{\{i \in dom iEdg (G) \| iEdg (G) (i) \subseteq S\}}) (x) = K \leftrightarrow (K \in ran iEdg (G) \land K \subseteq S))$
72	10 18 71	3bitrd	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in ran iEdg (H) \leftrightarrow (K \in ran iEdg (G) \land K \subseteq S))$
73		edgval	$⊢ Edg (H) = ran iEdg (H)$
74	4 73	eqtri	$⊢ I = ran iEdg (H)$
75	74	eleq2i	$⊢ K \in I \leftrightarrow K \in ran iEdg (H)$
76	2 42	eqtri	$⊢ E = ran iEdg (G)$
77	76	eleq2i	$⊢ K \in E \leftrightarrow K \in ran iEdg (G)$
78	77	anbi1i	$⊢ (K \in E \land K \subseteq S) \leftrightarrow (K \in ran iEdg (G) \land K \subseteq S)$
79	72 75 78	3bitr4g	$⊢ (G \in UHGraph \land S \subseteq V) \to (K \in I \leftrightarrow (K \in E \land K \subseteq S))$

Metamath Proof Explorer

Theorem isubgredg

Proof