Theorem brtpos

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

	Ref	Expression
Assertion	brtpos	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		brtpos2	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝐹 𝐶 ) ) )
2	1	adantr	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝐹 𝐶 ) ) )
3		opex	⊢ ⟨ 𝐵 , 𝐴 ⟩ ∈ V
4		breldmg	⊢ ( ( ⟨ 𝐵 , 𝐴 ⟩ ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) → ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 )
5	4	3expia	⊢ ( ( ⟨ 𝐵 , 𝐴 ⟩ ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 → ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 ) )
6	3 5	mpan	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 → ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 ) )
7	6	adantr	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 → ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 ) )
8		opelcnvg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ dom 𝐹 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 ) )
9	8	adantl	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ dom 𝐹 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ dom 𝐹 ) )
10	7 9	sylibrd	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ dom 𝐹 ) )
11		elun1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ dom 𝐹 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) )
12	10 11	syl6	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ) )
13	12	pm4.71rd	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) ) )
14		opswap	⊢ ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴 ⟩
15	14	breq1i	⊢ ( ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 )
16	15	anbi2i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝐹 𝐶 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )
17	13 16	bitr4di	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ∧ ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝐹 𝐶 ) ) )
18	2 17	bitr4d	⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )
19	18	ex	⊢ ( 𝐶 ∈ 𝑉 → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) ) )
20		brtpos0	⊢ ( 𝐶 ∈ 𝑉 → ( ∅ tpos 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) )
21		opprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
22	21	breq1d	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ∅ tpos 𝐹 𝐶 ) )
23		ancom	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
24		opprc	⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ⟨ 𝐵 , 𝐴 ⟩ = ∅ )
25	24	breq1d	⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) )
26	23 25	sylnbi	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) )
27	22 26	bibi12d	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) ↔ ( ∅ tpos 𝐹 𝐶 ↔ ∅ 𝐹 𝐶 ) ) )
28	20 27	syl5ibrcom	⊢ ( 𝐶 ∈ 𝑉 → ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) ) )
29	19 28	pm2.61d	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )