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→ABtposFC↔BAFC

Proof

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