This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-tpos

Description: Define the transposition of a function, which is a function G = tpos F satisfying G ( x , y ) = F ( y , x ) . (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$class F$
1	0	ctpos	$class tpos F$
2		vx	$setvar x$
3	0	cdm	$class dom F$
4	3	ccnv	$class {dom F}^{-1}$
5		c0	$class \emptyset$
6	5	csn	$class \{\emptyset\}$
7	4 6	cun	$class ({dom F}^{-1} \cup \{\emptyset\})$
8	2	cv	$setvar x$
9	8	csn	$class \{x\}$
10	9	ccnv	$class {\{x\}}^{-1}$
11	10	cuni	$class ⋃ {\{x\}}^{-1}$
12	2 7 11	cmpt	$class (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
13	0 12	ccom	$class (F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
14	1 13	wceq	$wff tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$