This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
uhgrvtxedgiedgb.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion uhgrvtxedgiedgb ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )

Proof

Step Hyp Ref Expression
1 uhgrvtxedgiedgb.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 uhgrvtxedgiedgb.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4 3 a1i ⊢ ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
5 1 rneqi ⊢ ran 𝐼 = ran ( iEdg ‘ 𝐺 )
6 4 2 5 3eqtr4g ⊢ ( 𝐺 ∈ UHGraph → 𝐸 = ran 𝐼 )
7 6 rexeqdv ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ↔ ∃ 𝑒 ∈ ran 𝐼 𝑈 ∈ 𝑒 ) )
8 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
9 8 funfnd ⊢ ( 𝐺 ∈ UHGraph → 𝐼 Fn dom 𝐼 )
10 eleq2 ⊢ ( 𝑒 = ( 𝐼 ‘ 𝑖 ) → ( 𝑈 ∈ 𝑒 ↔ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) )
11 10 rexrn ⊢ ( 𝐼 Fn dom 𝐼 → ( ∃ 𝑒 ∈ ran 𝐼 𝑈 ∈ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) )
12 9 11 syl ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑒 ∈ ran 𝐼 𝑈 ∈ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) )
13 7 12 bitrd ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) )
14 13 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ↔ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) )
15 14 bicomd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )