Metamath Proof Explorer

Theorem fv2ndcnv

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

Ref Expression
Assertion fv2ndcnv 
|- ( ( X e. V /\ Y e. A ) -> ( `' ( 2nd |` ( { X } X. A ) ) ` Y ) = <. X , Y >. )

Proof

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