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