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 e. UHGraph /\ U e. V ) -> ( E. i e. dom I U e. ( I ` i ) <-> E. e e. E U e. 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 e. UHGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
5	1	rneqi	|- ran I = ran ( iEdg ` G )
6	4 2 5	3eqtr4g	|- ( G e. UHGraph -> E = ran I )
7	6	rexeqdv	|- ( G e. UHGraph -> ( E. e e. E U e. e <-> E. e e. ran I U e. e ) )
8	1	uhgrfun	|- ( G e. UHGraph -> Fun I )
9	8	funfnd	|- ( G e. UHGraph -> I Fn dom I )
10		eleq2	|- ( e = ( I ` i ) -> ( U e. e <-> U e. ( I ` i ) ) )
11	10	rexrn	|- ( I Fn dom I -> ( E. e e. ran I U e. e <-> E. i e. dom I U e. ( I ` i ) ) )
12	9 11	syl	|- ( G e. UHGraph -> ( E. e e. ran I U e. e <-> E. i e. dom I U e. ( I ` i ) ) )
13	7 12	bitrd	|- ( G e. UHGraph -> ( E. e e. E U e. e <-> E. i e. dom I U e. ( I ` i ) ) )
14	13	adantr	|- ( ( G e. UHGraph /\ U e. V ) -> ( E. e e. E U e. e <-> E. i e. dom I U e. ( I ` i ) ) )
15	14	bicomd	|- ( ( G e. UHGraph /\ U e. V ) -> ( E. i e. dom I U e. ( I ` i ) <-> E. e e. E U e. e ) )