Metamath Proof Explorer

Theorem uhgrvtxedgiedgb

Description: In a hypergraph, a vertex is incident with an edge iff it is contained in an element of the range of the edge function. (Contributed by AV, 24-Dec-2020) (Revised by AV, 6-Jul-2022)

Ref Expression
Hypotheses uhgrvtxedgiedgb.i ⊢I=iEdg⁡G
uhgrvtxedgiedgb.e ⊢E=Edg⁡G
Assertion uhgrvtxedgiedgb ⊢G∈UHGraph∧U∈V→∃i∈dom⁡IU∈I⁡i↔∃e∈EU∈e

Proof

Step Hyp Ref Expression
1 uhgrvtxedgiedgb.i ⊢I=iEdg⁡G
2 uhgrvtxedgiedgb.e ⊢E=Edg⁡G
3 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
4 3 a1i ⊢G∈UHGraph→Edg⁡G=ran⁡iEdg⁡G
5 1 rneqi ⊢ran⁡I=ran⁡iEdg⁡G
6 4 2 5 3eqtr4g ⊢G∈UHGraph→E=ran⁡I
7 6 rexeqdv ⊢G∈UHGraph→∃e∈EU∈e↔∃e∈ran⁡IU∈e
8 1 uhgrfun ⊢G∈UHGraph→Fun⁡I
9 8 funfnd ⊢G∈UHGraph→IFndom⁡I
10 eleq2 ⊢e=I⁡i→U∈e↔U∈I⁡i
11 10 rexrn ⊢IFndom⁡I→∃e∈ran⁡IU∈e↔∃i∈dom⁡IU∈I⁡i
12 9 11 syl ⊢G∈UHGraph→∃e∈ran⁡IU∈e↔∃i∈dom⁡IU∈I⁡i
13 7 12 bitrd ⊢G∈UHGraph→∃e∈EU∈e↔∃i∈dom⁡IU∈I⁡i
14 13 adantr ⊢G∈UHGraph∧U∈V→∃e∈EU∈e↔∃i∈dom⁡IU∈I⁡i
15 14 bicomd ⊢G∈UHGraph∧U∈V→∃i∈dom⁡IU∈I⁡i↔∃e∈EU∈e