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 
|- 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 ) )