Metamath Proof Explorer

Theorem vtxdushgrfvedglem

Description: Lemma for vtxdushgrfvedg and vtxdusgrfvedg . (Contributed by AV, 12-Dec-2020) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypotheses vtxdushgrfvedg.v 
|- V = ( Vtx ` G )
vtxdushgrfvedg.e 
|- E = ( Edg ` G )
Assertion vtxdushgrfvedglem 
|- ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v 
 |-  V = ( Vtx ` G )
2 vtxdushgrfvedg.e 
 |-  E = ( Edg ` G )
3 fvex 
 |-  ( iEdg ` G ) e. _V
4 3 dmex 
 |-  dom ( iEdg ` G ) e. _V
5 4 rabex 
 |-  { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } e. _V
6 5 a1i 
 |-  ( ( G e. USHGraph /\ U e. V ) -> { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } e. _V )
7 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
8 eqid 
 |-  { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } = { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) }
9 eleq2w 
 |-  ( e = c -> ( U e. e <-> U e. c ) )
10 9 cbvrabv 
 |-  { e e. E | U e. e } = { c e. E | U e. c }
11 eqid 
 |-  ( x e. { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |-> ( ( iEdg ` G ) ` x ) ) = ( x e. { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |-> ( ( iEdg ` G ) ` x ) )
12 2 7 1 8 10 11 ushgredgedg 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( x e. { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |-> ( ( iEdg ` G ) ` x ) ) : { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } -1-1-onto-> { e e. E | U e. e } )
13 6 12 hasheqf1od 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )