dmtpos

Description: The domain of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	dmtpos	$⊢ Rel dom F \to dom tpos F = {dom F}^{-1}$

Step	Hyp	Ref	Expression
1		0nelxp	$⊢ \neg \emptyset \in (V \times V)$
2		ssel	$⊢ dom F \subseteq V \times V \to (\emptyset \in dom F \to \emptyset \in (V \times V))$
3	1 2	mtoi	$⊢ dom F \subseteq V \times V \to \neg \emptyset \in dom F$
4		df-rel	$⊢ Rel dom F \leftrightarrow dom F \subseteq V \times V$
5		reldmtpos	$⊢ Rel dom tpos F \leftrightarrow \neg \emptyset \in dom F$
6	3 4 5	3imtr4i	$⊢ Rel dom F \to Rel dom tpos F$
7		relcnv	$⊢ Rel {dom F}^{-1}$
8	6 7	jctir	$⊢ Rel dom F \to (Rel dom tpos F \land Rel {dom F}^{-1})$
9		vex	$⊢ z \in V$
10		brtpos	$⊢ z \in V \to (⟨x, y⟩ tpos F z \leftrightarrow ⟨y, x⟩ F z)$
11	9 10	mp1i	$⊢ Rel dom F \to (⟨x, y⟩ tpos F z \leftrightarrow ⟨y, x⟩ F z)$
12	11	exbidv	$⊢ Rel dom F \to (\exists z ⟨x, y⟩ tpos F z \leftrightarrow \exists z ⟨y, x⟩ F z)$
13		opex	$⊢ ⟨x, y⟩ \in V$
14	13	eldm	$⊢ ⟨x, y⟩ \in dom tpos F \leftrightarrow \exists z ⟨x, y⟩ tpos F z$
15		vex	$⊢ x \in V$
16		vex	$⊢ y \in V$
17	15 16	opelcnv	$⊢ ⟨x, y⟩ \in {dom F}^{-1} \leftrightarrow ⟨y, x⟩ \in dom F$
18		opex	$⊢ ⟨y, x⟩ \in V$
19	18	eldm	$⊢ ⟨y, x⟩ \in dom F \leftrightarrow \exists z ⟨y, x⟩ F z$
20	17 19	bitri	$⊢ ⟨x, y⟩ \in {dom F}^{-1} \leftrightarrow \exists z ⟨y, x⟩ F z$
21	12 14 20	3bitr4g	$⊢ Rel dom F \to (⟨x, y⟩ \in dom tpos F \leftrightarrow ⟨x, y⟩ \in {dom F}^{-1})$
22	21	eqrelrdv2	$⊢ ((Rel dom tpos F \land Rel {dom F}^{-1}) \land Rel dom F) \to dom tpos F = {dom F}^{-1}$
23	8 22	mpancom	$⊢ Rel dom F \to dom tpos F = {dom F}^{-1}$

Metamath Proof Explorer