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

Metamath Proof Explorer

Theorem uspgriedgedg

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

Ref Expression
Hypotheses uspgredgiedg.e 
|- E = ( Edg ` G )
uspgredgiedg.i 
|- I = ( iEdg ` G )
Assertion uspgriedgedg 
|- ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E 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 f1of 
 |-  ( I : dom I -1-1-onto-> ( Edg ` G ) -> I : dom I --> ( Edg ` G ) )
5 3 4 syl 
 |-  ( G e. USPGraph -> I : dom I --> ( Edg ` G ) )
6 feq3 
 |-  ( E = ( Edg ` G ) -> ( I : dom I --> E <-> I : dom I --> ( Edg ` G ) ) )
7 1 6 ax-mp 
 |-  ( I : dom I --> E <-> I : dom I --> ( Edg ` G ) )
8 5 7 sylibr 
 |-  ( G e. USPGraph -> I : dom I --> E )
9 fdmeu 
 |-  ( ( I : dom I --> E /\ X e. dom I ) -> E! k e. E ( I ` X ) = k )
10 8 9 sylan 
 |-  ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E ( I ` X ) = k )
11 eqcom 
 |-  ( k = ( I ` X ) <-> ( I ` X ) = k )
12 11 reubii 
 |-  ( E! k e. E k = ( I ` X ) <-> E! k e. E ( I ` X ) = k )
13 10 12 sylibr 
 |-  ( ( G e. USPGraph /\ X e. dom I ) -> E! k e. E k = ( I ` X ) )