Metamath Proof Explorer

Theorem fparlem1

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

Ref Expression
Assertion fparlem1 
|- ( `' ( 1st |` ( _V X. _V ) ) " { x } ) = ( { x } X. _V )

Proof

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