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 V = Vtx G
uhgrspan.e E = iEdg G
uhgrspan.s φ S W
uhgrspan.q φ Vtx S = V
uhgrspan.r φ iEdg S = E A
uhgrspan.g φ G UHGraph
Assertion uhgrspansubgrlem φ Edg S 𝒫 Vtx S

Proof

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