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