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
|- ( ph -> S e. W )
uhgrspan.q
|- ( ph -> ( Vtx ` S ) = V )
uhgrspan.r
|- ( ph -> ( iEdg ` S ) = ( E |` A ) )
uhgrspan.g
|- ( ph -> G e. UHGraph )
Assertion uhgrspansubgrlem
|- ( ph -> ( Edg ` S ) C_ ~P ( Vtx ` S ) )

Proof

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