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 V Y A 2 nd X × A -1 Y = X Y

Proof

Step Hyp Ref Expression
1 snidg X V X X
2 1 anim1i X V Y A X X Y A
3 eqid Y = Y
4 2 3 jctir X V Y A X X Y A Y = Y
5 2ndconst X V 2 nd X × A : X × A 1-1 onto A
6 5 adantr X V Y A 2 nd X × A : X × A 1-1 onto A
7 f1ocnv 2 nd X × A : X × A 1-1 onto A 2 nd X × A -1 : A 1-1 onto X × A
8 f1ofn 2 nd X × A -1 : A 1-1 onto X × A 2 nd X × A -1 Fn A
9 6 7 8 3syl X V Y A 2 nd X × A -1 Fn A
10 fnbrfvb 2 nd X × A -1 Fn A Y A 2 nd X × A -1 Y = X Y Y 2 nd X × A -1 X Y
11 9 10 sylancom X V Y A 2 nd X × A -1 Y = X Y Y 2 nd X × A -1 X Y
12 opex X Y V
13 brcnvg Y A X Y V Y 2 nd X × A -1 X Y X Y 2 nd X × A Y
14 12 13 mpan2 Y A Y 2 nd X × A -1 X Y X Y 2 nd X × A Y
15 14 adantl X V Y A Y 2 nd X × A -1 X Y X Y 2 nd X × A Y
16 brres Y A X Y 2 nd X × A Y X Y X × A X Y 2 nd Y
17 16 adantl X V Y A X Y 2 nd X × A Y X Y X × A X Y 2 nd Y
18 opelxp X Y X × A X X Y A
19 18 anbi1i X Y X × A X Y 2 nd Y X X Y A X Y 2 nd Y
20 br2ndeqg X V Y A X Y 2 nd Y Y = Y
21 20 anbi2d X V Y A X X Y A X Y 2 nd Y X X Y A Y = Y
22 19 21 syl5bb X V Y A X Y X × A X Y 2 nd Y X X Y A Y = Y
23 17 22 bitrd X V Y A X Y 2 nd X × A Y X X Y A Y = Y
24 15 23 bitrd X V Y A Y 2 nd X × A -1 X Y X X Y A Y = Y
25 11 24 bitrd X V Y A 2 nd X × A -1 Y = X Y X X Y A Y = Y
26 4 25 mpbird X V Y A 2 nd X × A -1 Y = X Y