tposfn2

Description: The domain of a transposition. (Contributed by NM, 10-Sep-2015)

		Ref	Expression
	Assertion	tposfn2	$⊢ Rel A \to (F Fn A \to tpos F Fn A^{-1})$

Step	Hyp	Ref	Expression
1		tposfun	$⊢ Fun F \to Fun tpos F$
2	1	a1i	$⊢ Rel A \to (Fun F \to Fun tpos F)$
3		dmtpos	$⊢ Rel dom F \to dom tpos F = {dom F}^{-1}$
4	3	a1i	$⊢ dom F = A \to (Rel dom F \to dom tpos F = {dom F}^{-1})$
5		releq	$⊢ dom F = A \to (Rel dom F \leftrightarrow Rel A)$
6		cnveq	$⊢ dom F = A \to {dom F}^{-1} = A^{-1}$
7	6	eqeq2d	$⊢ dom F = A \to (dom tpos F = {dom F}^{-1} \leftrightarrow dom tpos F = A^{-1})$
8	4 5 7	3imtr3d	$⊢ dom F = A \to (Rel A \to dom tpos F = A^{-1})$
9	8	com12	$⊢ Rel A \to (dom F = A \to dom tpos F = A^{-1})$
10	2 9	anim12d	$⊢ Rel A \to ((Fun F \land dom F = A) \to (Fun tpos F \land dom tpos F = A^{-1}))$
11		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
12		df-fn	$⊢ tpos F Fn A^{-1} \leftrightarrow (Fun tpos F \land dom tpos F = A^{-1})$
13	10 11 12	3imtr4g	$⊢ Rel A \to (F Fn A \to tpos F Fn A^{-1})$

Metamath Proof Explorer