mptcnv

Description: The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017)

		Ref	Expression
	Hypothesis	mptcnv.1	$⊢ φ \to ((x \in A \land y = B) \leftrightarrow (y \in C \land x = D))$
	Assertion	mptcnv	$⊢ φ \to {(x \in A ⟼ B)}^{-1} = (y \in C ⟼ D)$

Step	Hyp	Ref	Expression
1		mptcnv.1	$⊢ φ \to ((x \in A \land y = B) \leftrightarrow (y \in C \land x = D))$
2	1	opabbidv	$⊢ φ \to \{⟨y, x⟩ \| (x \in A \land y = B)\} = \{⟨y, x⟩ \| (y \in C \land x = D)\}$
3		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
4	3	cnveqi	$⊢ {(x \in A ⟼ B)}^{-1} = {\{⟨x, y⟩ \| (x \in A \land y = B)\}}^{-1}$
5		cnvopab	$⊢ {\{⟨x, y⟩ \| (x \in A \land y = B)\}}^{-1} = \{⟨y, x⟩ \| (x \in A \land y = B)\}$
6	4 5	eqtri	$⊢ {(x \in A ⟼ B)}^{-1} = \{⟨y, x⟩ \| (x \in A \land y = B)\}$
7		df-mpt	$⊢ (y \in C ⟼ D) = \{⟨y, x⟩ \| (y \in C \land x = D)\}$
8	2 6 7	3eqtr4g	$⊢ φ \to {(x \in A ⟼ B)}^{-1} = (y \in C ⟼ D)$

Metamath Proof Explorer