Metamath Proof Explorer

Theorem isubgredg

Description: An edge of an induced subgraph of a hypergraph is an edge of the hypergraph connecting vertices of the subgraph. (Contributed by AV, 24-Sep-2025)

Ref Expression
Hypotheses isubgredg.v 
|- V = ( Vtx ` G )
isubgredg.e 
|- E = ( Edg ` G )
isubgredg.h 
|- H = ( G ISubGr S )
isubgredg.i 
|- I = ( Edg ` H )
Assertion isubgredg 
|- ( ( G e. UHGraph /\ S C_ V ) -> ( K e. I <-> ( K e. E /\ K C_ S ) ) )

Proof

Step Hyp Ref Expression
1 isubgredg.v 
 |-  V = ( Vtx ` G )
2 isubgredg.e 
 |-  E = ( Edg ` G )
3 isubgredg.h 
 |-  H = ( G ISubGr S )
4 isubgredg.i 
 |-  I = ( Edg ` H )
5 3 fveq2i 
 |-  ( iEdg ` H ) = ( iEdg ` ( G ISubGr S ) )
6 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
7 1 6 isubgriedg 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) )
8 5 7 eqtrid 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` H ) = ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) )
9 8 rneqd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ran ( iEdg ` H ) = ran ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) )
10 9 eleq2d 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K e. ran ( iEdg ` H ) <-> K e. ran ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ) )
11 1 6 uhgrf 
 |-  ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
12 11 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
13 12 ffnd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
14 ssrab2 
 |-  { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } C_ dom ( iEdg ` G )
15 14 a1i 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } C_ dom ( iEdg ` G ) )
16 13 15 fnssresd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) Fn { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } )
17 fvelrnb 
 |-  ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) Fn { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } -> ( K e. ran ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) <-> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
18 16 17 syl 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K e. ran ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) <-> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
19 fvres 
 |-  ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } -> ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = ( ( iEdg ` G ) ` x ) )
20 19 adantl 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = ( ( iEdg ` G ) ` x ) )
21 20 eqeq1d 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K <-> ( ( iEdg ` G ) ` x ) = K ) )
22 fveq2 
 |-  ( i = x -> ( ( iEdg ` G ) ` i ) = ( ( iEdg ` G ) ` x ) )
23 22 sseq1d 
 |-  ( i = x -> ( ( ( iEdg ` G ) ` i ) C_ S <-> ( ( iEdg ` G ) ` x ) C_ S ) )
24 23 elrab 
 |-  ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } <-> ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) )
25 6 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
26 25 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> Fun ( iEdg ` G ) )
27 simpl 
 |-  ( ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) -> x e. dom ( iEdg ` G ) )
28 fvelrn 
 |-  ( ( Fun ( iEdg ` G ) /\ x e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) )
29 26 27 28 syl2anr 
 |-  ( ( ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) /\ ( G e. UHGraph /\ S C_ V ) ) -> ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) )
30 simpr 
 |-  ( ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) -> ( ( iEdg ` G ) ` x ) C_ S )
31 30 adantr 
 |-  ( ( ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) /\ ( G e. UHGraph /\ S C_ V ) ) -> ( ( iEdg ` G ) ` x ) C_ S )
32 29 31 jca 
 |-  ( ( ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) /\ ( G e. UHGraph /\ S C_ V ) ) -> ( ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) )
33 32 ex 
 |-  ( ( x e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) -> ( ( G e. UHGraph /\ S C_ V ) -> ( ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) ) )
34 24 33 sylbi 
 |-  ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } -> ( ( G e. UHGraph /\ S C_ V ) -> ( ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) ) )
35 34 impcom 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) )
36 eleq1 
 |-  ( ( ( iEdg ` G ) ` x ) = K -> ( ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) <-> K e. ran ( iEdg ` G ) ) )
37 sseq1 
 |-  ( ( ( iEdg ` G ) ` x ) = K -> ( ( ( iEdg ` G ) ` x ) C_ S <-> K C_ S ) )
38 36 37 anbi12d 
 |-  ( ( ( iEdg ` G ) ` x ) = K -> ( ( ( ( iEdg ` G ) ` x ) e. ran ( iEdg ` G ) /\ ( ( iEdg ` G ) ` x ) C_ S ) <-> ( K e. ran ( iEdg ` G ) /\ K C_ S ) ) )
39 35 38 syl5ibcom 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( ( ( iEdg ` G ) ` x ) = K -> ( K e. ran ( iEdg ` G ) /\ K C_ S ) ) )
40 21 39 sylbid 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K -> ( K e. ran ( iEdg ` G ) /\ K C_ S ) ) )
41 40 rexlimdva 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K -> ( K e. ran ( iEdg ` G ) /\ K C_ S ) ) )
42 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
43 42 eqcomi 
 |-  ran ( iEdg ` G ) = ( Edg ` G )
44 43 eleq2i 
 |-  ( K e. ran ( iEdg ` G ) <-> K e. ( Edg ` G ) )
45 6 edgiedgb 
 |-  ( Fun ( iEdg ` G ) -> ( K e. ( Edg ` G ) <-> E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) ) )
46 44 45 bitrid 
 |-  ( Fun ( iEdg ` G ) -> ( K e. ran ( iEdg ` G ) <-> E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) ) )
47 25 46 syl 
 |-  ( G e. UHGraph -> ( K e. ran ( iEdg ` G ) <-> E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) ) )
48 47 adantr 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K e. ran ( iEdg ` G ) <-> E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) ) )
49 simprl 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) -> x e. dom ( iEdg ` G ) )
50 simpr 
 |-  ( ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> K = ( ( iEdg ` G ) ` x ) )
51 50 sseq1d 
 |-  ( ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> ( K C_ S <-> ( ( iEdg ` G ) ` x ) C_ S ) )
52 51 biimpcd 
 |-  ( K C_ S -> ( ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> ( ( iEdg ` G ) ` x ) C_ S ) )
53 52 adantl 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) -> ( ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> ( ( iEdg ` G ) ` x ) C_ S ) )
54 53 imp 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) -> ( ( iEdg ` G ) ` x ) C_ S )
55 49 54 24 sylanbrc 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) -> x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } )
56 simpr 
 |-  ( ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } )
57 50 eqcomd 
 |-  ( ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> ( ( iEdg ` G ) ` x ) = K )
58 57 adantl 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) -> ( ( iEdg ` G ) ` x ) = K )
59 19 58 sylan9eqr 
 |-  ( ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K )
60 56 59 jca 
 |-  ( ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) /\ x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) -> ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } /\ ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
61 55 60 mpdan 
 |-  ( ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) /\ ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) ) -> ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } /\ ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
62 61 ex 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) -> ( ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } /\ ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) ) )
63 62 eximdv 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) -> ( E. x ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) -> E. x ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } /\ ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) ) )
64 df-rex 
 |-  ( E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) <-> E. x ( x e. dom ( iEdg ` G ) /\ K = ( ( iEdg ` G ) ` x ) ) )
65 df-rex 
 |-  ( E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K <-> E. x ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } /\ ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
66 63 64 65 3imtr4g 
 |-  ( ( ( G e. UHGraph /\ S C_ V ) /\ K C_ S ) -> ( E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) -> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
67 66 ex 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K C_ S -> ( E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) -> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) ) )
68 67 com23 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( E. x e. dom ( iEdg ` G ) K = ( ( iEdg ` G ) ` x ) -> ( K C_ S -> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) ) )
69 48 68 sylbid 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K e. ran ( iEdg ` G ) -> ( K C_ S -> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) ) )
70 69 impd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( ( K e. ran ( iEdg ` G ) /\ K C_ S ) -> E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K ) )
71 41 70 impbid 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( E. x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ( ( ( iEdg ` G ) |` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) C_ S } ) ` x ) = K <-> ( K e. ran ( iEdg ` G ) /\ K C_ S ) ) )
72 10 18 71 3bitrd 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K e. ran ( iEdg ` H ) <-> ( K e. ran ( iEdg ` G ) /\ K C_ S ) ) )
73 edgval 
 |-  ( Edg ` H ) = ran ( iEdg ` H )
74 4 73 eqtri 
 |-  I = ran ( iEdg ` H )
75 74 eleq2i 
 |-  ( K e. I <-> K e. ran ( iEdg ` H ) )
76 2 42 eqtri 
 |-  E = ran ( iEdg ` G )
77 76 eleq2i 
 |-  ( K e. E <-> K e. ran ( iEdg ` G ) )
78 77 anbi1i 
 |-  ( ( K e. E /\ K C_ S ) <-> ( K e. ran ( iEdg ` G ) /\ K C_ S ) )
79 72 75 78 3bitr4g 
 |-  ( ( G e. UHGraph /\ S C_ V ) -> ( K e. I <-> ( K e. E /\ K C_ S ) ) )