uhgrspansubgrlem

Description: Lemma for uhgrspansubgr : The edges of the graph S obtained by removing some edges of a hypergraph G are subsets of its vertices (a spanning subgraph, see comment for uhgrspansubgr . (Contributed by AV, 18-Nov-2020)

	Ref	Expression
Hypotheses	uhgrspan.v	$⊢ V = Vtx (G)$
	uhgrspan.e	$⊢ E = iEdg (G)$
	uhgrspan.s	$⊢ φ \to S \in W$
	uhgrspan.q	$⊢ φ \to Vtx (S) = V$
	uhgrspan.r	$⊢ φ \to iEdg (S) = {E ↾}_{A}$
	uhgrspan.g	$⊢ φ \to G \in UHGraph$
Assertion	uhgrspansubgrlem	$⊢ φ \to Edg (S) \subseteq 𝒫 Vtx (S)$

Proof

Step	Hyp	Ref	Expression
1		uhgrspan.v	$⊢ V = Vtx (G)$
2		uhgrspan.e	$⊢ E = iEdg (G)$
3		uhgrspan.s	$⊢ φ \to S \in W$
4		uhgrspan.q	$⊢ φ \to Vtx (S) = V$
5		uhgrspan.r	$⊢ φ \to iEdg (S) = {E ↾}_{A}$
6		uhgrspan.g	$⊢ φ \to G \in UHGraph$
7		edgval	$⊢ Edg (S) = ran iEdg (S)$
8	7	eleq2i	$⊢ e \in Edg (S) \leftrightarrow e \in ran iEdg (S)$
9	2	uhgrfun	$⊢ G \in UHGraph \to Fun E$
10		funres	$⊢ Fun E \to Fun ({E ↾}_{A})$
11	6 9 10	3syl	$⊢ φ \to Fun ({E ↾}_{A})$
12	5	funeqd	$⊢ φ \to (Fun iEdg (S) \leftrightarrow Fun ({E ↾}_{A}))$
13	11 12	mpbird	$⊢ φ \to Fun iEdg (S)$
14		elrnrexdmb	$⊢ Fun iEdg (S) \to (e \in ran iEdg (S) \leftrightarrow \exists i \in dom iEdg (S) e = iEdg (S) (i))$
15	13 14	syl	$⊢ φ \to (e \in ran iEdg (S) \leftrightarrow \exists i \in dom iEdg (S) e = iEdg (S) (i))$
16	5	adantr	$⊢ (φ \land i \in dom iEdg (S)) \to iEdg (S) = {E ↾}_{A}$
17	16	fveq1d	$⊢ (φ \land i \in dom iEdg (S)) \to iEdg (S) (i) = ({E ↾}_{A}) (i)$
18	5	dmeqd	$⊢ φ \to dom iEdg (S) = dom ({E ↾}_{A})$
19		dmres	$⊢ dom ({E ↾}_{A}) = A \cap dom E$
20	18 19	eqtrdi	$⊢ φ \to dom iEdg (S) = A \cap dom E$
21	20	eleq2d	$⊢ φ \to (i \in dom iEdg (S) \leftrightarrow i \in (A \cap dom E))$
22		elinel1	$⊢ i \in (A \cap dom E) \to i \in A$
23	21 22	biimtrdi	$⊢ φ \to (i \in dom iEdg (S) \to i \in A)$
24	23	imp	$⊢ (φ \land i \in dom iEdg (S)) \to i \in A$
25	24	fvresd	$⊢ (φ \land i \in dom iEdg (S)) \to ({E ↾}_{A}) (i) = E (i)$
26	17 25	eqtrd	$⊢ (φ \land i \in dom iEdg (S)) \to iEdg (S) (i) = E (i)$
27		elinel2	$⊢ i \in (A \cap dom E) \to i \in dom E$
28	21 27	biimtrdi	$⊢ φ \to (i \in dom iEdg (S) \to i \in dom E)$
29	28	imp	$⊢ (φ \land i \in dom iEdg (S)) \to i \in dom E$
30	1 2	uhgrss	$⊢ (G \in UHGraph \land i \in dom E) \to E (i) \subseteq V$
31	6 29 30	syl2an2r	$⊢ (φ \land i \in dom iEdg (S)) \to E (i) \subseteq V$
32	4	pweqd	$⊢ φ \to 𝒫 Vtx (S) = 𝒫 V$
33	32	eleq2d	$⊢ φ \to (E (i) \in 𝒫 Vtx (S) \leftrightarrow E (i) \in 𝒫 V)$
34	33	adantr	$⊢ (φ \land i \in dom iEdg (S)) \to (E (i) \in 𝒫 Vtx (S) \leftrightarrow E (i) \in 𝒫 V)$
35		fvex	$⊢ E (i) \in V$
36	35	elpw	$⊢ E (i) \in 𝒫 V \leftrightarrow E (i) \subseteq V$
37	34 36	bitrdi	$⊢ (φ \land i \in dom iEdg (S)) \to (E (i) \in 𝒫 Vtx (S) \leftrightarrow E (i) \subseteq V)$
38	31 37	mpbird	$⊢ (φ \land i \in dom iEdg (S)) \to E (i) \in 𝒫 Vtx (S)$
39	26 38	eqeltrd	$⊢ (φ \land i \in dom iEdg (S)) \to iEdg (S) (i) \in 𝒫 Vtx (S)$
40		eleq1	$⊢ e = iEdg (S) (i) \to (e \in 𝒫 Vtx (S) \leftrightarrow iEdg (S) (i) \in 𝒫 Vtx (S))$
41	39 40	syl5ibrcom	$⊢ (φ \land i \in dom iEdg (S)) \to (e = iEdg (S) (i) \to e \in 𝒫 Vtx (S))$
42	41	rexlimdva	$⊢ φ \to (\exists i \in dom iEdg (S) e = iEdg (S) (i) \to e \in 𝒫 Vtx (S))$
43	15 42	sylbid	$⊢ φ \to (e \in ran iEdg (S) \to e \in 𝒫 Vtx (S))$
44	8 43	biimtrid	$⊢ φ \to (e \in Edg (S) \to e \in 𝒫 Vtx (S))$
45	44	ssrdv	$⊢ φ \to Edg (S) \subseteq 𝒫 Vtx (S)$

Metamath Proof Explorer

Theorem uhgrspansubgrlem

Proof