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