tposmpo

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

		Ref	Expression
	Hypothesis	tposmpo.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	tposmpo	$⊢ tpos F = (y \in B, x \in A ⟼ C)$

Step	Hyp	Ref	Expression
1		tposmpo.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
3		ancom	$⊢ (x \in A \land y \in B) \leftrightarrow (y \in B \land x \in A)$
4	3	anbi1i	$⊢ ((x \in A \land y \in B) \land z = C) \leftrightarrow ((y \in B \land x \in A) \land z = C)$
5	4	oprabbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{⟨⟨x, y⟩, z⟩ \| ((y \in B \land x \in A) \land z = C)\}$
6	1 2 5	3eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((y \in B \land x \in A) \land z = C)\}$
7	6	tposoprab	$⊢ tpos F = \{⟨⟨y, x⟩, z⟩ \| ((y \in B \land x \in A) \land z = C)\}$
8		df-mpo	$⊢ (y \in B, x \in A ⟼ C) = \{⟨⟨y, x⟩, z⟩ \| ((y \in B \land x \in A) \land z = C)\}$
9	7 8	eqtr4i	$⊢ tpos F = (y \in B, x \in A ⟼ C)$

Metamath Proof Explorer