dftpos3

Description: Alternate definition of tpos when F has relational domain. Compare df-cnv . (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	dftpos3	$⊢ Rel dom F \to tpos F = \{⟨⟨x, y⟩, z⟩ \| ⟨y, x⟩ F z\}$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel {dom F}^{-1}$
2		dmtpos	$⊢ Rel dom F \to dom tpos F = {dom F}^{-1}$
3	2	releqd	$⊢ Rel dom F \to (Rel dom tpos F \leftrightarrow Rel {dom F}^{-1})$
4	1 3	mpbiri	$⊢ Rel dom F \to Rel dom tpos F$
5		reltpos	$⊢ Rel tpos F$
6	4 5	jctil	$⊢ Rel dom F \to (Rel tpos F \land Rel dom tpos F)$
7		relrelss	$⊢ (Rel tpos F \land Rel dom tpos F) \leftrightarrow tpos F \subseteq (V \times V) \times V$
8	6 7	sylib	$⊢ Rel dom F \to tpos F \subseteq (V \times V) \times V$
9	8	sseld	$⊢ Rel dom F \to (w \in tpos F \to w \in ((V \times V) \times V))$
10		elvvv	$⊢ w \in ((V \times V) \times V) \leftrightarrow \exists x \exists y \exists z w = ⟨⟨x, y⟩, z⟩$
11	9 10	imbitrdi	$⊢ Rel dom F \to (w \in tpos F \to \exists x \exists y \exists z w = ⟨⟨x, y⟩, z⟩)$
12	11	pm4.71rd	$⊢ Rel dom F \to (w \in tpos F \leftrightarrow (\exists x \exists y \exists z w = ⟨⟨x, y⟩, z⟩ \land w \in tpos F))$
13		19.41vvv	$⊢ \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land w \in tpos F) \leftrightarrow (\exists x \exists y \exists z w = ⟨⟨x, y⟩, z⟩ \land w \in tpos F)$
14		eleq1	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (w \in tpos F \leftrightarrow ⟨⟨x, y⟩, z⟩ \in tpos F)$
15		df-br	$⊢ ⟨x, y⟩ tpos F z \leftrightarrow ⟨⟨x, y⟩, z⟩ \in tpos F$
16		brtpos	$⊢ z \in V \to (⟨x, y⟩ tpos F z \leftrightarrow ⟨y, x⟩ F z)$
17	16	elv	$⊢ ⟨x, y⟩ tpos F z \leftrightarrow ⟨y, x⟩ F z$
18	15 17	bitr3i	$⊢ ⟨⟨x, y⟩, z⟩ \in tpos F \leftrightarrow ⟨y, x⟩ F z$
19	14 18	bitrdi	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (w \in tpos F \leftrightarrow ⟨y, x⟩ F z)$
20	19	pm5.32i	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land w \in tpos F) \leftrightarrow (w = ⟨⟨x, y⟩, z⟩ \land ⟨y, x⟩ F z)$
21	20	3exbii	$⊢ \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land w \in tpos F) \leftrightarrow \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ⟨y, x⟩ F z)$
22	13 21	bitr3i	$⊢ (\exists x \exists y \exists z w = ⟨⟨x, y⟩, z⟩ \land w \in tpos F) \leftrightarrow \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ⟨y, x⟩ F z)$
23	12 22	bitrdi	$⊢ Rel dom F \to (w \in tpos F \leftrightarrow \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ⟨y, x⟩ F z))$
24	23	eqabdv	$⊢ Rel dom F \to tpos F = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ⟨y, x⟩ F z)\}$
25		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ⟨y, x⟩ F z\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land ⟨y, x⟩ F z)\}$
26	24 25	eqtr4di	$⊢ Rel dom F \to tpos F = \{⟨⟨x, y⟩, z⟩ \| ⟨y, x⟩ F z\}$

Metamath Proof Explorer

Theorem dftpos3

Proof