Metamath Proof Explorer

Theorem tposmpo

Description: Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis tposmpo.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
Assertion tposmpo ⊢ tpos F = y ∈ B , x ∈ A ⟼ C

Proof

Step Hyp Ref Expression
1 tposmpo.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C
3 ancom ⊢ x ∈ A ∧ y ∈ B ↔ y ∈ B ∧ x ∈ A
4 3 anbi1i ⊢ x ∈ A ∧ y ∈ B ∧ z = C ↔ y ∈ B ∧ x ∈ A ∧ z = C
5 4 oprabbii ⊢ x y z | x ∈ A ∧ y ∈ B ∧ z = C = x y z | y ∈ B ∧ x ∈ A ∧ z = C
6 1 2 5 3eqtri ⊢ F = x y z | y ∈ B ∧ x ∈ A ∧ z = C
7 6 tposoprab ⊢ tpos F = y x z | y ∈ B ∧ x ∈ A ∧ z = C
8 df-mpo ⊢ y ∈ B , x ∈ A ⟼ C = y x z | y ∈ B ∧ x ∈ A ∧ z = C
9 7 8 eqtr4i ⊢ tpos F = y ∈ B , x ∈ A ⟼ C