Metamath Proof Explorer


Theorem brtpos2

Description: Value of the transposition at a pair <. A , B >. . (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion brtpos2 B V A tpos F B A dom F -1 A -1 F B

Proof

Step Hyp Ref Expression
1 reltpos Rel tpos F
2 1 brrelex1i A tpos F B A V
3 2 a1i B V A tpos F B A V
4 elex A dom F -1 A V
5 4 adantr A dom F -1 A -1 F B A V
6 5 a1i B V A dom F -1 A -1 F B A V
7 df-tpos tpos F = F x dom F -1 x -1
8 7 breqi A tpos F B A F x dom F -1 x -1 B
9 brcog A V B V A F x dom F -1 x -1 B y A x dom F -1 x -1 y y F B
10 8 9 syl5bb A V B V A tpos F B y A x dom F -1 x -1 y y F B
11 funmpt Fun x dom F -1 x -1
12 funbrfv2b Fun x dom F -1 x -1 A x dom F -1 x -1 y A dom x dom F -1 x -1 x dom F -1 x -1 A = y
13 11 12 ax-mp A x dom F -1 x -1 y A dom x dom F -1 x -1 x dom F -1 x -1 A = y
14 snex x V
15 14 cnvex x -1 V
16 15 uniex x -1 V
17 eqid x dom F -1 x -1 = x dom F -1 x -1
18 16 17 dmmpti dom x dom F -1 x -1 = dom F -1
19 18 eleq2i A dom x dom F -1 x -1 A dom F -1
20 eqcom x dom F -1 x -1 A = y y = x dom F -1 x -1 A
21 19 20 anbi12i A dom x dom F -1 x -1 x dom F -1 x -1 A = y A dom F -1 y = x dom F -1 x -1 A
22 sneq x = A x = A
23 22 cnveqd x = A x -1 = A -1
24 23 unieqd x = A x -1 = A -1
25 snex A V
26 25 cnvex A -1 V
27 26 uniex A -1 V
28 24 17 27 fvmpt A dom F -1 x dom F -1 x -1 A = A -1
29 28 eqeq2d A dom F -1 y = x dom F -1 x -1 A y = A -1
30 29 pm5.32i A dom F -1 y = x dom F -1 x -1 A A dom F -1 y = A -1
31 21 30 bitri A dom x dom F -1 x -1 x dom F -1 x -1 A = y A dom F -1 y = A -1
32 13 31 bitri A x dom F -1 x -1 y A dom F -1 y = A -1
33 32 biancomi A x dom F -1 x -1 y y = A -1 A dom F -1
34 33 anbi1i A x dom F -1 x -1 y y F B y = A -1 A dom F -1 y F B
35 anass y = A -1 A dom F -1 y F B y = A -1 A dom F -1 y F B
36 34 35 bitri A x dom F -1 x -1 y y F B y = A -1 A dom F -1 y F B
37 36 exbii y A x dom F -1 x -1 y y F B y y = A -1 A dom F -1 y F B
38 breq1 y = A -1 y F B A -1 F B
39 38 anbi2d y = A -1 A dom F -1 y F B A dom F -1 A -1 F B
40 27 39 ceqsexv y y = A -1 A dom F -1 y F B A dom F -1 A -1 F B
41 37 40 bitri y A x dom F -1 x -1 y y F B A dom F -1 A -1 F B
42 10 41 bitrdi A V B V A tpos F B A dom F -1 A -1 F B
43 42 expcom B V A V A tpos F B A dom F -1 A -1 F B
44 3 6 43 pm5.21ndd B V A tpos F B A dom F -1 A -1 F B