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

Metamath Proof Explorer

Theorem uspgredg2vlem

Description: Lemma for uspgredg2v . (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 6-Dec-2020)

Ref Expression
Hypotheses uspgredg2v.v 
|- V = ( Vtx ` G )
uspgredg2v.e 
|- E = ( Edg ` G )
uspgredg2v.a 
|- A = { e e. E | N e. e }
Assertion uspgredg2vlem 
|- ( ( G e. USPGraph /\ Y e. A ) -> ( iota_ z e. V Y = { N , z } ) e. V )

Proof

Step Hyp Ref Expression
1 uspgredg2v.v 
 |-  V = ( Vtx ` G )
2 uspgredg2v.e 
 |-  E = ( Edg ` G )
3 uspgredg2v.a 
 |-  A = { e e. E | N e. e }
4 eleq2 
 |-  ( e = Y -> ( N e. e <-> N e. Y ) )
5 4 3 elrab2 
 |-  ( Y e. A <-> ( Y e. E /\ N e. Y ) )
6 simpl 
 |-  ( ( G e. USPGraph /\ ( Y e. E /\ N e. Y ) ) -> G e. USPGraph )
7 2 eleq2i 
 |-  ( Y e. E <-> Y e. ( Edg ` G ) )
8 7 biimpi 
 |-  ( Y e. E -> Y e. ( Edg ` G ) )
9 8 ad2antrl 
 |-  ( ( G e. USPGraph /\ ( Y e. E /\ N e. Y ) ) -> Y e. ( Edg ` G ) )
10 simprr 
 |-  ( ( G e. USPGraph /\ ( Y e. E /\ N e. Y ) ) -> N e. Y )
11 6 9 10 3jca 
 |-  ( ( G e. USPGraph /\ ( Y e. E /\ N e. Y ) ) -> ( G e. USPGraph /\ Y e. ( Edg ` G ) /\ N e. Y ) )
12 uspgredg2vtxeu 
 |-  ( ( G e. USPGraph /\ Y e. ( Edg ` G ) /\ N e. Y ) -> E! z e. ( Vtx ` G ) Y = { N , z } )
13 reueq1 
 |-  ( V = ( Vtx ` G ) -> ( E! z e. V Y = { N , z } <-> E! z e. ( Vtx ` G ) Y = { N , z } ) )
14 1 13 ax-mp 
 |-  ( E! z e. V Y = { N , z } <-> E! z e. ( Vtx ` G ) Y = { N , z } )
15 12 14 sylibr 
 |-  ( ( G e. USPGraph /\ Y e. ( Edg ` G ) /\ N e. Y ) -> E! z e. V Y = { N , z } )
16 riotacl 
 |-  ( E! z e. V Y = { N , z } -> ( iota_ z e. V Y = { N , z } ) e. V )
17 11 15 16 3syl 
 |-  ( ( G e. USPGraph /\ ( Y e. E /\ N e. Y ) ) -> ( iota_ z e. V Y = { N , z } ) e. V )
18 5 17 sylan2b 
 |-  ( ( G e. USPGraph /\ Y e. A ) -> ( iota_ z e. V Y = { N , z } ) e. V )