Metamath Proof Explorer

Theorem 1stpreimas

Description: The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020)

Ref Expression
Assertion 1stpreimas 
|- ( ( Rel A /\ X e. V ) -> ( `' ( 1st |` A ) " { X } ) = ( { X } X. ( A " { X } ) ) )

Proof

Step Hyp Ref Expression
1 1st2ndb 
 |-  ( z e. ( _V X. _V ) <-> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
2 1 biimpi 
 |-  ( z e. ( _V X. _V ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
3 2 ad2antrl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
4 fvex 
 |-  ( 1st ` z ) e. _V
5 4 elsn 
 |-  ( ( 1st ` z ) e. { X } <-> ( 1st ` z ) = X )
6 5 biimpi 
 |-  ( ( 1st ` z ) e. { X } -> ( 1st ` z ) = X )
7 6 ad2antrl 
 |-  ( ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) -> ( 1st ` z ) = X )
8 7 adantl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> ( 1st ` z ) = X )
9 8 opeq1d 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> <. ( 1st ` z ) , ( 2nd ` z ) >. = <. X , ( 2nd ` z ) >. )
10 3 9 eqtrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> z = <. X , ( 2nd ` z ) >. )
11 simplr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> X e. V )
12 simprrr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> ( 2nd ` z ) e. ( A " { X } ) )
13 elimasng 
 |-  ( ( X e. V /\ ( 2nd ` z ) e. ( A " { X } ) ) -> ( ( 2nd ` z ) e. ( A " { X } ) <-> <. X , ( 2nd ` z ) >. e. A ) )
14 13 biimpa 
 |-  ( ( ( X e. V /\ ( 2nd ` z ) e. ( A " { X } ) ) /\ ( 2nd ` z ) e. ( A " { X } ) ) -> <. X , ( 2nd ` z ) >. e. A )
15 11 12 12 14 syl21anc 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> <. X , ( 2nd ` z ) >. e. A )
16 10 15 eqeltrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> z e. A )
17 fvres 
 |-  ( z e. A -> ( ( 1st |` A ) ` z ) = ( 1st ` z ) )
18 16 17 syl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> ( ( 1st |` A ) ` z ) = ( 1st ` z ) )
19 18 8 eqtrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> ( ( 1st |` A ) ` z ) = X )
20 16 19 jca 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) -> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) )
21 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
22 21 birani 
 |-  ( ( Rel A /\ X e. V ) -> A C_ ( _V X. _V ) )
23 22 sselda 
 |-  ( ( ( Rel A /\ X e. V ) /\ z e. A ) -> z e. ( _V X. _V ) )
24 23 adantrr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z e. ( _V X. _V ) )
25 17 ad2antrl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( ( 1st |` A ) ` z ) = ( 1st ` z ) )
26 simprr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( ( 1st |` A ) ` z ) = X )
27 25 26 eqtr3d 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( 1st ` z ) = X )
28 27 5 sylibr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( 1st ` z ) e. { X } )
29 27 28 eqeltrrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> X e. { X } )
30 simpr 
 |-  ( ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) /\ x = X ) -> x = X )
31 30 opeq1d 
 |-  ( ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) /\ x = X ) -> <. x , ( 2nd ` z ) >. = <. X , ( 2nd ` z ) >. )
32 31 eleq1d 
 |-  ( ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) /\ x = X ) -> ( <. x , ( 2nd ` z ) >. e. A <-> <. X , ( 2nd ` z ) >. e. A ) )
33 1st2nd 
 |-  ( ( Rel A /\ z e. A ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
34 33 ad2ant2r 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
35 27 opeq1d 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> <. ( 1st ` z ) , ( 2nd ` z ) >. = <. X , ( 2nd ` z ) >. )
36 34 35 eqtrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z = <. X , ( 2nd ` z ) >. )
37 simprl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z e. A )
38 36 37 eqeltrrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> <. X , ( 2nd ` z ) >. e. A )
39 29 32 38 rspcedvd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> E. x e. { X } <. x , ( 2nd ` z ) >. e. A )
40 df-rex 
 |-  ( E. x e. { X } <. x , ( 2nd ` z ) >. e. A <-> E. x ( x e. { X } /\ <. x , ( 2nd ` z ) >. e. A ) )
41 39 40 sylib 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> E. x ( x e. { X } /\ <. x , ( 2nd ` z ) >. e. A ) )
42 fvex 
 |-  ( 2nd ` z ) e. _V
43 42 elima3 
 |-  ( ( 2nd ` z ) e. ( A " { X } ) <-> E. x ( x e. { X } /\ <. x , ( 2nd ` z ) >. e. A ) )
44 41 43 sylibr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( 2nd ` z ) e. ( A " { X } ) )
45 28 44 jca 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) )
46 24 45 jca 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) )
47 20 46 impbida 
 |-  ( ( Rel A /\ X e. V ) -> ( ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) )
48 elxp7 
 |-  ( z e. ( { X } X. ( A " { X } ) ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) )
49 48 a1i 
 |-  ( ( Rel A /\ X e. V ) -> ( z e. ( { X } X. ( A " { X } ) ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) ) )
50 fo1st 
 |-  1st : _V -onto-> _V
51 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
52 50 51 ax-mp 
 |-  1st Fn _V
53 ssv 
 |-  A C_ _V
54 fnssres 
 |-  ( ( 1st Fn _V /\ A C_ _V ) -> ( 1st |` A ) Fn A )
55 52 53 54 mp2an 
 |-  ( 1st |` A ) Fn A
56 fniniseg 
 |-  ( ( 1st |` A ) Fn A -> ( z e. ( `' ( 1st |` A ) " { X } ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) )
57 55 56 ax-mp 
 |-  ( z e. ( `' ( 1st |` A ) " { X } ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) )
58 57 a1i 
 |-  ( ( Rel A /\ X e. V ) -> ( z e. ( `' ( 1st |` A ) " { X } ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) )
59 47 49 58 3bitr4rd 
 |-  ( ( Rel A /\ X e. V ) -> ( z e. ( `' ( 1st |` A ) " { X } ) <-> z e. ( { X } X. ( A " { X } ) ) ) )
60 59 eqrdv 
 |-  ( ( Rel A /\ X e. V ) -> ( `' ( 1st |` A ) " { X } ) = ( { X } X. ( A " { X } ) ) )