Metamath Proof Explorer

Theorem subgruhgredgd

Description: An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020) (Revised by AV, 21-Nov-2020)

Ref Expression
Hypotheses subgruhgredgd.v 
|- V = ( Vtx ` S )
subgruhgredgd.i 
|- I = ( iEdg ` S )
subgruhgredgd.g 
|- ( ph -> G e. UHGraph )
subgruhgredgd.s 
|- ( ph -> S SubGraph G )
subgruhgredgd.x 
|- ( ph -> X e. dom I )
Assertion subgruhgredgd 
|- ( ph -> ( I ` X ) e. ( ~P V \ { (/) } ) )

Proof

Step Hyp Ref Expression
1 subgruhgredgd.v 
 |-  V = ( Vtx ` S )
2 subgruhgredgd.i 
 |-  I = ( iEdg ` S )
3 subgruhgredgd.g 
 |-  ( ph -> G e. UHGraph )
4 subgruhgredgd.s 
 |-  ( ph -> S SubGraph G )
5 subgruhgredgd.x 
 |-  ( ph -> X e. dom I )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
8 eqid 
 |-  ( Edg ` S ) = ( Edg ` S )
9 1 6 2 7 8 subgrprop2 
 |-  ( S SubGraph G -> ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) )
10 4 9 syl 
 |-  ( ph -> ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) )
11 simpr3 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( Edg ` S ) C_ ~P V )
12 subgruhgrfun 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
13 3 4 12 syl2anc 
 |-  ( ph -> Fun ( iEdg ` S ) )
14 2 dmeqi 
 |-  dom I = dom ( iEdg ` S )
15 5 14 eleqtrdi 
 |-  ( ph -> X e. dom ( iEdg ` S ) )
16 13 15 jca 
 |-  ( ph -> ( Fun ( iEdg ` S ) /\ X e. dom ( iEdg ` S ) ) )
17 16 adantr 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( Fun ( iEdg ` S ) /\ X e. dom ( iEdg ` S ) ) )
18 2 fveq1i 
 |-  ( I ` X ) = ( ( iEdg ` S ) ` X )
19 fvelrn 
 |-  ( ( Fun ( iEdg ` S ) /\ X e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` X ) e. ran ( iEdg ` S ) )
20 18 19 eqeltrid 
 |-  ( ( Fun ( iEdg ` S ) /\ X e. dom ( iEdg ` S ) ) -> ( I ` X ) e. ran ( iEdg ` S ) )
21 17 20 syl 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( I ` X ) e. ran ( iEdg ` S ) )
22 edgval 
 |-  ( Edg ` S ) = ran ( iEdg ` S )
23 21 22 eleqtrrdi 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( I ` X ) e. ( Edg ` S ) )
24 11 23 sseldd 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( I ` X ) e. ~P V )
25 7 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
26 3 25 syl 
 |-  ( ph -> Fun ( iEdg ` G ) )
27 26 adantr 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> Fun ( iEdg ` G ) )
28 simpr2 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> I C_ ( iEdg ` G ) )
29 5 adantr 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> X e. dom I )
30 funssfv 
 |-  ( ( Fun ( iEdg ` G ) /\ I C_ ( iEdg ` G ) /\ X e. dom I ) -> ( ( iEdg ` G ) ` X ) = ( I ` X ) )
31 30 eqcomd 
 |-  ( ( Fun ( iEdg ` G ) /\ I C_ ( iEdg ` G ) /\ X e. dom I ) -> ( I ` X ) = ( ( iEdg ` G ) ` X ) )
32 27 28 29 31 syl3anc 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( I ` X ) = ( ( iEdg ` G ) ` X ) )
33 3 adantr 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> G e. UHGraph )
34 26 funfnd 
 |-  ( ph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
35 34 adantr 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
36 subgreldmiedg 
 |-  ( ( S SubGraph G /\ X e. dom ( iEdg ` S ) ) -> X e. dom ( iEdg ` G ) )
37 4 15 36 syl2anc 
 |-  ( ph -> X e. dom ( iEdg ` G ) )
38 37 adantr 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> X e. dom ( iEdg ` G ) )
39 7 uhgrn0 
 |-  ( ( G e. UHGraph /\ ( iEdg ` G ) Fn dom ( iEdg ` G ) /\ X e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` X ) =/= (/) )
40 33 35 38 39 syl3anc 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( ( iEdg ` G ) ` X ) =/= (/) )
41 32 40 eqnetrd 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( I ` X ) =/= (/) )
42 eldifsn 
 |-  ( ( I ` X ) e. ( ~P V \ { (/) } ) <-> ( ( I ` X ) e. ~P V /\ ( I ` X ) =/= (/) ) )
43 24 41 42 sylanbrc 
 |-  ( ( ph /\ ( V C_ ( Vtx ` G ) /\ I C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P V ) ) -> ( I ` X ) e. ( ~P V \ { (/) } ) )
44 10 43 mpdan 
 |-  ( ph -> ( I ` X ) e. ( ~P V \ { (/) } ) )