This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ‘ 𝑆 ) )