Metamath Proof Explorer

Theorem usgredg2vlem2

Description: Lemma 2 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 usgredg2vlem2 
|- ( ( G e. USGraph /\ Y e. A ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) )

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 6 biimpi 
 |-  ( Y e. A -> ( Y e. dom E /\ N e. ( E ` Y ) ) )
8 1 2 usgredgreu 
 |-  ( ( G e. USGraph /\ Y e. dom E /\ N e. ( E ` Y ) ) -> E! z e. V ( E ` Y ) = { N , z } )
9 8 3expb 
 |-  ( ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) -> E! z e. V ( E ` Y ) = { N , z } )
10 1 2 3 usgredg2vlem1 
 |-  ( ( G e. USGraph /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
11 10 adantlr 
 |-  ( ( ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) /\ Y e. A ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
12 11 ad4ant23 
 |-  ( ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) /\ I = ( iota_ z e. V ( E ` Y ) = { z , N } ) ) -> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V )
13 eleq1 
 |-  ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( I e. V <-> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V ) )
14 13 adantl 
 |-  ( ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) /\ I = ( iota_ z e. V ( E ` Y ) = { z , N } ) ) -> ( I e. V <-> ( iota_ z e. V ( E ` Y ) = { z , N } ) e. V ) )
15 12 14 mpbird 
 |-  ( ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) /\ I = ( iota_ z e. V ( E ` Y ) = { z , N } ) ) -> I e. V )
16 prcom 
 |-  { N , z } = { z , N }
17 16 eqeq2i 
 |-  ( ( E ` Y ) = { N , z } <-> ( E ` Y ) = { z , N } )
18 17 reubii 
 |-  ( E! z e. V ( E ` Y ) = { N , z } <-> E! z e. V ( E ` Y ) = { z , N } )
19 18 biimpi 
 |-  ( E! z e. V ( E ` Y ) = { N , z } -> E! z e. V ( E ` Y ) = { z , N } )
20 19 ad3antrrr 
 |-  ( ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) /\ I = ( iota_ z e. V ( E ` Y ) = { z , N } ) ) -> E! z e. V ( E ` Y ) = { z , N } )
21 preq1 
 |-  ( z = I -> { z , N } = { I , N } )
22 21 eqeq2d 
 |-  ( z = I -> ( ( E ` Y ) = { z , N } <-> ( E ` Y ) = { I , N } ) )
23 22 riota2 
 |-  ( ( I e. V /\ E! z e. V ( E ` Y ) = { z , N } ) -> ( ( E ` Y ) = { I , N } <-> ( iota_ z e. V ( E ` Y ) = { z , N } ) = I ) )
24 15 20 23 syl2anc 
 |-  ( ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) /\ I = ( iota_ z e. V ( E ` Y ) = { z , N } ) ) -> ( ( E ` Y ) = { I , N } <-> ( iota_ z e. V ( E ` Y ) = { z , N } ) = I ) )
25 24 exbiri 
 |-  ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( ( iota_ z e. V ( E ` Y ) = { z , N } ) = I -> ( E ` Y ) = { I , N } ) ) )
26 25 com13 
 |-  ( ( iota_ z e. V ( E ` Y ) = { z , N } ) = I -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) -> ( E ` Y ) = { I , N } ) ) )
27 26 eqcoms 
 |-  ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) -> ( E ` Y ) = { I , N } ) ) )
28 27 pm2.43i 
 |-  ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) /\ Y e. A ) -> ( E ` Y ) = { I , N } ) )
29 28 expdcom 
 |-  ( ( E! z e. V ( E ` Y ) = { N , z } /\ ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) ) -> ( Y e. A -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) ) )
30 9 29 mpancom 
 |-  ( ( G e. USGraph /\ ( Y e. dom E /\ N e. ( E ` Y ) ) ) -> ( Y e. A -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) ) )
31 30 expcom 
 |-  ( ( Y e. dom E /\ N e. ( E ` Y ) ) -> ( G e. USGraph -> ( Y e. A -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) ) ) )
32 31 com23 
 |-  ( ( Y e. dom E /\ N e. ( E ` Y ) ) -> ( Y e. A -> ( G e. USGraph -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) ) ) )
33 7 32 mpcom 
 |-  ( Y e. A -> ( G e. USGraph -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) ) )
34 33 impcom 
 |-  ( ( G e. USGraph /\ Y e. A ) -> ( I = ( iota_ z e. V ( E ` Y ) = { z , N } ) -> ( E ` Y ) = { I , N } ) )