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

Metamath Proof Explorer

Theorem uspgredgiedg

Description: In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025)

Ref Expression
Hypotheses uspgredgiedg.e 
|- E = ( Edg ` G )
uspgredgiedg.i 
|- I = ( iEdg ` G )
Assertion uspgredgiedg 
|- ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I K = ( I ` x ) )

Proof

Step Hyp Ref Expression
1 uspgredgiedg.e 
 |-  E = ( Edg ` G )
2 uspgredgiedg.i 
 |-  I = ( iEdg ` G )
3 2 uspgrf1oedg 
 |-  ( G e. USPGraph -> I : dom I -1-1-onto-> ( Edg ` G ) )
4 f1oeq3 
 |-  ( E = ( Edg ` G ) -> ( I : dom I -1-1-onto-> E <-> I : dom I -1-1-onto-> ( Edg ` G ) ) )
5 1 4 ax-mp 
 |-  ( I : dom I -1-1-onto-> E <-> I : dom I -1-1-onto-> ( Edg ` G ) )
6 3 5 sylibr 
 |-  ( G e. USPGraph -> I : dom I -1-1-onto-> E )
7 f1ofveu 
 |-  ( ( I : dom I -1-1-onto-> E /\ K e. E ) -> E! x e. dom I ( I ` x ) = K )
8 6 7 sylan 
 |-  ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I ( I ` x ) = K )
9 eqcom 
 |-  ( K = ( I ` x ) <-> ( I ` x ) = K )
10 9 reubii 
 |-  ( E! x e. dom I K = ( I ` x ) <-> E! x e. dom I ( I ` x ) = K )
11 8 10 sylibr 
 |-  ( ( G e. USPGraph /\ K e. E ) -> E! x e. dom I K = ( I ` x ) )