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 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ∃ 𝑒 ∈ 𝐸 𝑈 ∈ 𝑒 ) )