dftpos2

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

		Ref	Expression
	Assertion	dftpos2	$⊢ Rel dom F \to tpos F = F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$

Step	Hyp	Ref	Expression
1		dmtpos	$⊢ Rel dom F \to dom tpos F = {dom F}^{-1}$
2	1	reseq2d	$⊢ Rel dom F \to {tpos F ↾}_{dom tpos F} = {tpos F ↾}_{{dom F}^{-1}}$
3		reltpos	$⊢ Rel tpos F$
4		resdm	$⊢ Rel tpos F \to {tpos F ↾}_{dom tpos F} = tpos F$
5	3 4	ax-mp	$⊢ {tpos F ↾}_{dom tpos F} = tpos F$
6		df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
7	6	reseq1i	$⊢ {tpos F ↾}_{{dom F}^{-1}} = {(F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) ↾}_{{dom F}^{-1}}$
8		resco	$⊢ {(F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) ↾}_{{dom F}^{-1}} = F \circ ({(x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{{dom F}^{-1}})$
9		ssun1	$⊢ {dom F}^{-1} \subseteq {dom F}^{-1} \cup \{\emptyset\}$
10		resmpt	$⊢ {dom F}^{-1} \subseteq {dom F}^{-1} \cup \{\emptyset\} \to {(x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{{dom F}^{-1}} = (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$
11	9 10	ax-mp	$⊢ {(x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{{dom F}^{-1}} = (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$
12	11	coeq2i	$⊢ F \circ ({(x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{{dom F}^{-1}}) = F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$
13	7 8 12	3eqtri	$⊢ {tpos F ↾}_{{dom F}^{-1}} = F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$
14	2 5 13	3eqtr3g	$⊢ Rel dom F \to tpos F = F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$

Metamath Proof Explorer