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 biimpi 
 |-  ( Rel A -> A C_ ( _V X. _V ) )
23 22 adantr 
 |-  ( ( Rel A /\ X e. V ) -> A C_ ( _V X. _V ) )
24 23 sselda 
 |-  ( ( ( Rel A /\ X e. V ) /\ z e. A ) -> z e. ( _V X. _V ) )
25 24 adantrr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z e. ( _V X. _V ) )
26 17 ad2antrl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( ( 1st |` A ) ` z ) = ( 1st ` z ) )
27 simprr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( ( 1st |` A ) ` z ) = X )
28 26 27 eqtr3d 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( 1st ` z ) = X )
29 28 5 sylibr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( 1st ` z ) e. { X } )
30 28 29 eqeltrrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> X e. { X } )
31 simpr 
 |-  ( ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) /\ x = X ) -> x = X )
32 31 opeq1d 
 |-  ( ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) /\ x = X ) -> <. x , ( 2nd ` z ) >. = <. X , ( 2nd ` z ) >. )
33 32 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 ) )
34 1st2nd 
 |-  ( ( Rel A /\ z e. A ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
35 34 ad2ant2r 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
36 28 opeq1d 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> <. ( 1st ` z ) , ( 2nd ` z ) >. = <. X , ( 2nd ` z ) >. )
37 35 36 eqtrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z = <. X , ( 2nd ` z ) >. )
38 simprl 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> z e. A )
39 37 38 eqeltrrd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> <. X , ( 2nd ` z ) >. e. A )
40 30 33 39 rspcedvd 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> E. x e. { X } <. x , ( 2nd ` z ) >. e. A )
41 df-rex 
 |-  ( E. x e. { X } <. x , ( 2nd ` z ) >. e. A <-> E. x ( x e. { X } /\ <. x , ( 2nd ` z ) >. e. A ) )
42 40 41 sylib 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> E. x ( x e. { X } /\ <. x , ( 2nd ` z ) >. e. A ) )
43 fvex 
 |-  ( 2nd ` z ) e. _V
44 43 elima3 
 |-  ( ( 2nd ` z ) e. ( A " { X } ) <-> E. x ( x e. { X } /\ <. x , ( 2nd ` z ) >. e. A ) )
45 42 44 sylibr 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( 2nd ` z ) e. ( A " { X } ) )
46 29 45 jca 
 |-  ( ( ( Rel A /\ X e. V ) /\ ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) -> ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) )
47 25 46 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 } ) ) ) )
48 20 47 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 ) ) )
49 elxp7 
 |-  ( z e. ( { X } X. ( A " { X } ) ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. { X } /\ ( 2nd ` z ) e. ( A " { X } ) ) ) )
50 49 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 } ) ) ) ) )
51 fo1st 
 |-  1st : _V -onto-> _V
52 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
53 51 52 ax-mp 
 |-  1st Fn _V
54 ssv 
 |-  A C_ _V
55 fnssres 
 |-  ( ( 1st Fn _V /\ A C_ _V ) -> ( 1st |` A ) Fn A )
56 53 54 55 mp2an 
 |-  ( 1st |` A ) Fn A
57 fniniseg 
 |-  ( ( 1st |` A ) Fn A -> ( z e. ( `' ( 1st |` A ) " { X } ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) )
58 56 57 ax-mp 
 |-  ( z e. ( `' ( 1st |` A ) " { X } ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) )
59 58 a1i 
 |-  ( ( Rel A /\ X e. V ) -> ( z e. ( `' ( 1st |` A ) " { X } ) <-> ( z e. A /\ ( ( 1st |` A ) ` z ) = X ) ) )
60 48 50 59 3bitr4rd 
 |-  ( ( Rel A /\ X e. V ) -> ( z e. ( `' ( 1st |` A ) " { X } ) <-> z e. ( { X } X. ( A " { X } ) ) ) )
61 60 eqrdv 
 |-  ( ( Rel A /\ X e. V ) -> ( `' ( 1st |` A ) " { X } ) = ( { X } X. ( A " { X } ) ) )