Metamath Proof Explorer


Theorem brtpos

Description: The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion brtpos C V A B tpos F C B A F C

Proof

Step Hyp Ref Expression
1 brtpos2 C V A B tpos F C A B dom F -1 A B -1 F C
2 1 adantr C V A V B V A B tpos F C A B dom F -1 A B -1 F C
3 opex B A V
4 breldmg B A V C V B A F C B A dom F
5 4 3expia B A V C V B A F C B A dom F
6 3 5 mpan C V B A F C B A dom F
7 6 adantr C V A V B V B A F C B A dom F
8 opelcnvg A V B V A B dom F -1 B A dom F
9 8 adantl C V A V B V A B dom F -1 B A dom F
10 7 9 sylibrd C V A V B V B A F C A B dom F -1
11 elun1 A B dom F -1 A B dom F -1
12 10 11 syl6 C V A V B V B A F C A B dom F -1
13 12 pm4.71rd C V A V B V B A F C A B dom F -1 B A F C
14 opswap A B -1 = B A
15 14 breq1i A B -1 F C B A F C
16 15 anbi2i A B dom F -1 A B -1 F C A B dom F -1 B A F C
17 13 16 bitr4di C V A V B V B A F C A B dom F -1 A B -1 F C
18 2 17 bitr4d C V A V B V A B tpos F C B A F C
19 18 ex C V A V B V A B tpos F C B A F C
20 brtpos0 C V tpos F C F C
21 opprc ¬ A V B V A B =
22 21 breq1d ¬ A V B V A B tpos F C tpos F C
23 ancom A V B V B V A V
24 opprc ¬ B V A V B A =
25 24 breq1d ¬ B V A V B A F C F C
26 23 25 sylnbi ¬ A V B V B A F C F C
27 22 26 bibi12d ¬ A V B V A B tpos F C B A F C tpos F C F C
28 20 27 syl5ibrcom C V ¬ A V B V A B tpos F C B A F C
29 19 28 pm2.61d C V A B tpos F C B A F C