Metamath Proof Explorer

Theorem usgredg2vlem1

Description: Lemma 1 for usgredg2v . (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgredg2v.v 
|- V = ( Vtx ` G )
usgredg2v.e 
|- E = ( iEdg ` G )
usgredg2v.a 
|- A = { x e. dom E | N e. ( E ` x ) }
Assertion usgredg2vlem1 
|- ( ( G e. USGraph /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )

Proof

Step Hyp Ref Expression
1 usgredg2v.v 
 |-  V = ( Vtx ` G )
2 usgredg2v.e 
 |-  E = ( iEdg ` G )
3 usgredg2v.a 
 |-  A = { x e. dom E | N e. ( E ` x ) }
4 fveq2 
 |-  ( x = Y -> ( E ` x ) = ( E ` Y ) )
5 4 eleq2d 
 |-  ( x = Y -> ( N e. ( E ` x ) <-> N e. ( E ` Y ) ) )
6 5 3 elrab2 
 |-  ( Y e. A <-> ( Y e. dom E /\ N e. ( E ` Y ) ) )
7 1 2 usgredgreu 
 |-  ( ( G e. USGraph /\ Y e. dom E /\ N e. ( E ` Y ) ) -> E! z e. V ( E ` Y ) = { N , z } )
8 prcom 
 |-  { N , z } = { z , N }
9 8 eqeq2i 
 |-  ( ( E ` Y ) = { N , z } <-> ( E ` Y ) = { z , N } )
10 9 reubii 
 |-  ( E! z e. V ( E ` Y ) = { N , z } <-> E! z e. V ( E ` Y ) = { z , N } )
11 7 10 sylib 
 |-  ( ( G e. USGraph /\ Y e. dom E /\ N e. ( E ` Y ) ) -> E! z e. V ( E ` Y ) = { z , N } )
12 11 3expb 
 |-  ( ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) -> E! z e. V ( E ` Y ) = { z , N } )
13 riotacl 
 |-  ( E! z e. V ( E ` Y ) = { z , N } -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
14 12 13 syl 
 |-  ( ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
15 6 14 sylan2b 
 |-  ( ( G e. USGraph /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )