Metamath Proof Explorer

Theorem fparlem2

Description: Lemma for fpar . (Contributed by NM, 22-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fparlem2 
|- ( `' ( 2nd |` ( _V X. _V ) ) " { y } ) = ( _V X. { y } )

Proof

Step Hyp Ref Expression
1 fvres 
 |-  ( x e. ( _V X. _V ) -> ( ( 2nd |` ( _V X. _V ) ) ` x ) = ( 2nd ` x ) )
2 1 eqeq1d 
 |-  ( x e. ( _V X. _V ) -> ( ( ( 2nd |` ( _V X. _V ) ) ` x ) = y <-> ( 2nd ` x ) = y ) )
3 vex 
 |-  y e. _V
4 3 elsn2 
 |-  ( ( 2nd ` x ) e. { y } <-> ( 2nd ` x ) = y )
5 fvex 
 |-  ( 1st ` x ) e. _V
6 5 biantrur 
 |-  ( ( 2nd ` x ) e. { y } <-> ( ( 1st ` x ) e. _V /\ ( 2nd ` x ) e. { y } ) )
7 4 6 bitr3i 
 |-  ( ( 2nd ` x ) = y <-> ( ( 1st ` x ) e. _V /\ ( 2nd ` x ) e. { y } ) )
8 2 7 bitrdi 
 |-  ( x e. ( _V X. _V ) -> ( ( ( 2nd |` ( _V X. _V ) ) ` x ) = y <-> ( ( 1st ` x ) e. _V /\ ( 2nd ` x ) e. { y } ) ) )
9 8 pm5.32i 
 |-  ( ( x e. ( _V X. _V ) /\ ( ( 2nd |` ( _V X. _V ) ) ` x ) = y ) <-> ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. _V /\ ( 2nd ` x ) e. { y } ) ) )
10 f2ndres 
 |-  ( 2nd |` ( _V X. _V ) ) : ( _V X. _V ) --> _V
11 ffn 
 |-  ( ( 2nd |` ( _V X. _V ) ) : ( _V X. _V ) --> _V -> ( 2nd |` ( _V X. _V ) ) Fn ( _V X. _V ) )
12 fniniseg 
 |-  ( ( 2nd |` ( _V X. _V ) ) Fn ( _V X. _V ) -> ( x e. ( `' ( 2nd |` ( _V X. _V ) ) " { y } ) <-> ( x e. ( _V X. _V ) /\ ( ( 2nd |` ( _V X. _V ) ) ` x ) = y ) ) )
13 10 11 12 mp2b 
 |-  ( x e. ( `' ( 2nd |` ( _V X. _V ) ) " { y } ) <-> ( x e. ( _V X. _V ) /\ ( ( 2nd |` ( _V X. _V ) ) ` x ) = y ) )
14 elxp7 
 |-  ( x e. ( _V X. { y } ) <-> ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. _V /\ ( 2nd ` x ) e. { y } ) ) )
15 9 13 14 3bitr4i 
 |-  ( x e. ( `' ( 2nd |` ( _V X. _V ) ) " { y } ) <-> x e. ( _V X. { y } ) )
16 15 eqriv 
 |-  ( `' ( 2nd |` ( _V X. _V ) ) " { y } ) = ( _V X. { y } )