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 ⁡ I U ∈ I ⁡ i ↔ ∃ e ∈ E U ∈ 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 ∈ E U ∈ e ↔ ∃ e ∈ ran ⁡ I U ∈ e
8 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
9 8 funfnd ⊢ G ∈ UHGraph → I Fn dom ⁡ I
10 eleq2 ⊢ e = I ⁡ i → U ∈ e ↔ U ∈ I ⁡ i
11 10 rexrn ⊢ I Fn dom ⁡ I → ∃ e ∈ ran ⁡ I U ∈ e ↔ ∃ i ∈ dom ⁡ I U ∈ I ⁡ i
12 9 11 syl ⊢ G ∈ UHGraph → ∃ e ∈ ran ⁡ I U ∈ e ↔ ∃ i ∈ dom ⁡ I U ∈ I ⁡ i
13 7 12 bitrd ⊢ G ∈ UHGraph → ∃ e ∈ E U ∈ e ↔ ∃ i ∈ dom ⁡ I U ∈ I ⁡ i
14 13 adantr ⊢ G ∈ UHGraph ∧ U ∈ V → ∃ e ∈ E U ∈ e ↔ ∃ i ∈ dom ⁡ I U ∈ I ⁡ i
15 14 bicomd ⊢ G ∈ UHGraph ∧ U ∈ V → ∃ i ∈ dom ⁡ I U ∈ I ⁡ i ↔ ∃ e ∈ E U ∈ e