subgruhgredgd

Description: An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020) (Revised by AV, 21-Nov-2020)

	Ref	Expression
Hypotheses	subgruhgredgd.v	$⊢ V = Vtx (S)$
	subgruhgredgd.i	$⊢ I = iEdg (S)$
	subgruhgredgd.g	$⊢ φ \to G \in UHGraph$
	subgruhgredgd.s	$⊢ φ \to S SubGraph G$
	subgruhgredgd.x	$⊢ φ \to X \in dom I$
Assertion	subgruhgredgd	$⊢ φ \to I (X) \in (𝒫 V ∖ \{\emptyset\})$

Proof

Step	Hyp	Ref	Expression
1		subgruhgredgd.v	$⊢ V = Vtx (S)$
2		subgruhgredgd.i	$⊢ I = iEdg (S)$
3		subgruhgredgd.g	$⊢ φ \to G \in UHGraph$
4		subgruhgredgd.s	$⊢ φ \to S SubGraph G$
5		subgruhgredgd.x	$⊢ φ \to X \in dom I$
6		eqid	$⊢ Vtx (G) = Vtx (G)$
7		eqid	$⊢ iEdg (G) = iEdg (G)$
8		eqid	$⊢ Edg (S) = Edg (S)$
9	1 6 2 7 8	subgrprop2	$⊢ S SubGraph G \to (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)$
10	4 9	syl	$⊢ φ \to (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)$
11		simpr3	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to Edg (S) \subseteq 𝒫 V$
12		subgruhgrfun	$⊢ (G \in UHGraph \land S SubGraph G) \to Fun iEdg (S)$
13	3 4 12	syl2anc	$⊢ φ \to Fun iEdg (S)$
14	2	dmeqi	$⊢ dom I = dom iEdg (S)$
15	5 14	eleqtrdi	$⊢ φ \to X \in dom iEdg (S)$
16	13 15	jca	$⊢ φ \to (Fun iEdg (S) \land X \in dom iEdg (S))$
17	16	adantr	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to (Fun iEdg (S) \land X \in dom iEdg (S))$
18	2	fveq1i	$⊢ I (X) = iEdg (S) (X)$
19		fvelrn	$⊢ (Fun iEdg (S) \land X \in dom iEdg (S)) \to iEdg (S) (X) \in ran iEdg (S)$
20	18 19	eqeltrid	$⊢ (Fun iEdg (S) \land X \in dom iEdg (S)) \to I (X) \in ran iEdg (S)$
21	17 20	syl	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I (X) \in ran iEdg (S)$
22		edgval	$⊢ Edg (S) = ran iEdg (S)$
23	21 22	eleqtrrdi	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I (X) \in Edg (S)$
24	11 23	sseldd	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I (X) \in 𝒫 V$
25	7	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
26	3 25	syl	$⊢ φ \to Fun iEdg (G)$
27	26	adantr	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to Fun iEdg (G)$
28		simpr2	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I \subseteq iEdg (G)$
29	5	adantr	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to X \in dom I$
30		funssfv	$⊢ (Fun iEdg (G) \land I \subseteq iEdg (G) \land X \in dom I) \to iEdg (G) (X) = I (X)$
31	30	eqcomd	$⊢ (Fun iEdg (G) \land I \subseteq iEdg (G) \land X \in dom I) \to I (X) = iEdg (G) (X)$
32	27 28 29 31	syl3anc	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I (X) = iEdg (G) (X)$
33	3	adantr	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to G \in UHGraph$
34	26	funfnd	$⊢ φ \to iEdg (G) Fn dom iEdg (G)$
35	34	adantr	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to iEdg (G) Fn dom iEdg (G)$
36		subgreldmiedg	$⊢ (S SubGraph G \land X \in dom iEdg (S)) \to X \in dom iEdg (G)$
37	4 15 36	syl2anc	$⊢ φ \to X \in dom iEdg (G)$
38	37	adantr	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to X \in dom iEdg (G)$
39	7	uhgrn0	$⊢ (G \in UHGraph \land iEdg (G) Fn dom iEdg (G) \land X \in dom iEdg (G)) \to iEdg (G) (X) \neq \emptyset$
40	33 35 38 39	syl3anc	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to iEdg (G) (X) \neq \emptyset$
41	32 40	eqnetrd	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I (X) \neq \emptyset$
42		eldifsn	$⊢ I (X) \in (𝒫 V ∖ \{\emptyset\}) \leftrightarrow (I (X) \in 𝒫 V \land I (X) \neq \emptyset)$
43	24 41 42	sylanbrc	$⊢ (φ \land (V \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 V)) \to I (X) \in (𝒫 V ∖ \{\emptyset\})$
44	10 43	mpdan	$⊢ φ \to I (X) \in (𝒫 V ∖ \{\emptyset\})$

Metamath Proof Explorer

Theorem subgruhgredgd

Proof