Metamath Proof Explorer


Theorem 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 syl6bi ( 𝜑 → ( 𝑖 ∈ 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 syl6bi ( 𝜑 → ( 𝑖 ∈ 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 syl5bi ( 𝜑 → ( 𝑒 ∈ ( Edg ‘ 𝑆 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
45 44 ssrdv ( 𝜑 → ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )