Metamath Proof Explorer

Theorem fv1stcnv

Description: The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020)

Ref Expression
Assertion fv1stcnv 
|- ( ( X e. A /\ Y e. V ) -> ( `' ( 1st |` ( A X. { Y } ) ) ` X ) = <. X , Y >. )

Proof

Step Hyp Ref Expression
1 snidg 
 |-  ( Y e. V -> Y e. { Y } )
2 1 anim2i 
 |-  ( ( X e. A /\ Y e. V ) -> ( X e. A /\ Y e. { Y } ) )
3 eqid 
 |-  X = X
4 2 3 jctir 
 |-  ( ( X e. A /\ Y e. V ) -> ( ( X e. A /\ Y e. { Y } ) /\ X = X ) )
5 opex 
 |-  <. X , Y >. e. _V
6 brcnvg 
 |-  ( ( X e. A /\ <. X , Y >. e. _V ) -> ( X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. <-> <. X , Y >. ( 1st |` ( A X. { Y } ) ) X ) )
7 5 6 mpan2 
 |-  ( X e. A -> ( X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. <-> <. X , Y >. ( 1st |` ( A X. { Y } ) ) X ) )
8 brres 
 |-  ( X e. A -> ( <. X , Y >. ( 1st |` ( A X. { Y } ) ) X <-> ( <. X , Y >. e. ( A X. { Y } ) /\ <. X , Y >. 1st X ) ) )
9 7 8 bitrd 
 |-  ( X e. A -> ( X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. <-> ( <. X , Y >. e. ( A X. { Y } ) /\ <. X , Y >. 1st X ) ) )
10 9 adantr 
 |-  ( ( X e. A /\ Y e. V ) -> ( X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. <-> ( <. X , Y >. e. ( A X. { Y } ) /\ <. X , Y >. 1st X ) ) )
11 opelxp 
 |-  ( <. X , Y >. e. ( A X. { Y } ) <-> ( X e. A /\ Y e. { Y } ) )
12 11 anbi1i 
 |-  ( ( <. X , Y >. e. ( A X. { Y } ) /\ <. X , Y >. 1st X ) <-> ( ( X e. A /\ Y e. { Y } ) /\ <. X , Y >. 1st X ) )
13 br1steqg 
 |-  ( ( X e. A /\ Y e. V ) -> ( <. X , Y >. 1st X <-> X = X ) )
14 13 anbi2d 
 |-  ( ( X e. A /\ Y e. V ) -> ( ( ( X e. A /\ Y e. { Y } ) /\ <. X , Y >. 1st X ) <-> ( ( X e. A /\ Y e. { Y } ) /\ X = X ) ) )
15 12 14 syl5bb 
 |-  ( ( X e. A /\ Y e. V ) -> ( ( <. X , Y >. e. ( A X. { Y } ) /\ <. X , Y >. 1st X ) <-> ( ( X e. A /\ Y e. { Y } ) /\ X = X ) ) )
16 10 15 bitrd 
 |-  ( ( X e. A /\ Y e. V ) -> ( X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. <-> ( ( X e. A /\ Y e. { Y } ) /\ X = X ) ) )
17 4 16 mpbird 
 |-  ( ( X e. A /\ Y e. V ) -> X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. )
18 1stconst 
 |-  ( Y e. V -> ( 1st |` ( A X. { Y } ) ) : ( A X. { Y } ) -1-1-onto-> A )
19 f1ocnv 
 |-  ( ( 1st |` ( A X. { Y } ) ) : ( A X. { Y } ) -1-1-onto-> A -> `' ( 1st |` ( A X. { Y } ) ) : A -1-1-onto-> ( A X. { Y } ) )
20 f1ofn 
 |-  ( `' ( 1st |` ( A X. { Y } ) ) : A -1-1-onto-> ( A X. { Y } ) -> `' ( 1st |` ( A X. { Y } ) ) Fn A )
21 18 19 20 3syl 
 |-  ( Y e. V -> `' ( 1st |` ( A X. { Y } ) ) Fn A )
22 simpl 
 |-  ( ( X e. A /\ Y e. V ) -> X e. A )
23 fnbrfvb 
 |-  ( ( `' ( 1st |` ( A X. { Y } ) ) Fn A /\ X e. A ) -> ( ( `' ( 1st |` ( A X. { Y } ) ) ` X ) = <. X , Y >. <-> X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. ) )
24 21 22 23 syl2an2 
 |-  ( ( X e. A /\ Y e. V ) -> ( ( `' ( 1st |` ( A X. { Y } ) ) ` X ) = <. X , Y >. <-> X `' ( 1st |` ( A X. { Y } ) ) <. X , Y >. ) )
25 17 24 mpbird 
 |-  ( ( X e. A /\ Y e. V ) -> ( `' ( 1st |` ( A X. { Y } ) ) ` X ) = <. X , Y >. )