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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uhgrspan.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	uhgrspan.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	uhgrspan.q	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
	uhgrspan.r	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
	uhgrspan.g	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
Assertion	uhgrspansubgrlem	⊢ ( 𝜑 → ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		uhgrspan.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uhgrspan.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		uhgrspan.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
4		uhgrspan.q	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
5		uhgrspan.r	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
6		uhgrspan.g	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
7		edgval	⊢ ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 )
8	7	eleq2i	⊢ ( 𝑒 ∈ ( Edg ‘ 𝑆 ) ↔ 𝑒 ∈ ran ( iEdg ‘ 𝑆 ) )
9	2	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
10		funres	⊢ ( Fun 𝐸 → Fun ( 𝐸 ↾ 𝐴 ) )
11	6 9 10	3syl	⊢ ( 𝜑 → Fun ( 𝐸 ↾ 𝐴 ) )
12	5	funeqd	⊢ ( 𝜑 → ( Fun ( iEdg ‘ 𝑆 ) ↔ Fun ( 𝐸 ↾ 𝐴 ) ) )
13	11 12	mpbird	⊢ ( 𝜑 → Fun ( iEdg ‘ 𝑆 ) )
14		elrnrexdmb	⊢ ( Fun ( iEdg ‘ 𝑆 ) → ( 𝑒 ∈ ran ( iEdg ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) 𝑒 = ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝑒 ∈ ran ( iEdg ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) 𝑒 = ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
16	5	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
17	16	fveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) = ( ( 𝐸 ↾ 𝐴 ) ‘ 𝑖 ) )
18	5	dmeqd	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = dom ( 𝐸 ↾ 𝐴 ) )
19		dmres	⊢ dom ( 𝐸 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐸 )
20	18 19	eqtrdi	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = ( 𝐴 ∩ dom 𝐸 ) )
21	20	eleq2d	⊢ ( 𝜑 → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ↔ 𝑖 ∈ ( 𝐴 ∩ dom 𝐸 ) ) )
22		elinel1	⊢ ( 𝑖 ∈ ( 𝐴 ∩ dom 𝐸 ) → 𝑖 ∈ 𝐴 )
23	21 22	biimtrdi	⊢ ( 𝜑 → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → 𝑖 ∈ 𝐴 ) )
24	23	imp	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑖 ∈ 𝐴 )
25	24	fvresd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( 𝐸 ↾ 𝐴 ) ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )
26	17 25	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )
27		elinel2	⊢ ( 𝑖 ∈ ( 𝐴 ∩ dom 𝐸 ) → 𝑖 ∈ dom 𝐸 )
28	21 27	biimtrdi	⊢ ( 𝜑 → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → 𝑖 ∈ dom 𝐸 ) )
29	28	imp	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑖 ∈ dom 𝐸 )
30	1 2	uhgrss	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑖 ) ⊆ 𝑉 )
31	6 29 30	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐸 ‘ 𝑖 ) ⊆ 𝑉 )
32	4	pweqd	⊢ ( 𝜑 → 𝒫 ( Vtx ‘ 𝑆 ) = 𝒫 𝑉 )
33	32	eleq2d	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) ↔ ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 𝑉 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) ↔ ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 𝑉 ) )
35		fvex	⊢ ( 𝐸 ‘ 𝑖 ) ∈ V
36	35	elpw	⊢ ( ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 𝑉 ↔ ( 𝐸 ‘ 𝑖 ) ⊆ 𝑉 )
37	34 36	bitrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) ↔ ( 𝐸 ‘ 𝑖 ) ⊆ 𝑉 ) )
38	31 37	mpbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐸 ‘ 𝑖 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) )
39	26 38	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) )
40		eleq1	⊢ ( 𝑒 = ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ↔ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
41	39 40	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝑒 = ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
42	41	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) 𝑒 = ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
43	15 42	sylbid	⊢ ( 𝜑 → ( 𝑒 ∈ ran ( iEdg ‘ 𝑆 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
44	8 43	biimtrid	⊢ ( 𝜑 → ( 𝑒 ∈ ( Edg ‘ 𝑆 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
45	44	ssrdv	⊢ ( 𝜑 → ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )

Metamath Proof Explorer

Theorem uhgrspansubgrlem

Proof