tposresg

Description: The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025)

		Ref	Expression
	Assertion	tposresg	$⊢ {tpos F ↾}_{R} = ({tpos F ↾}_{{R^{-1}}^{-1}}) \cup ({F ↾}_{(R \cap \{\emptyset\})})$

Proof

Step	Hyp	Ref	Expression
1		rescom	$⊢ {({tpos F ↾}_{((V \times V) \cup \{\emptyset\})}) ↾}_{R} = {({tpos F ↾}_{R}) ↾}_{((V \times V) \cup \{\emptyset\})}$
2		reltpos	$⊢ Rel tpos F$
3		dmtposss	$⊢ dom tpos F \subseteq (V \times V) \cup \{\emptyset\}$
4		relssres	$⊢ (Rel tpos F \land dom tpos F \subseteq (V \times V) \cup \{\emptyset\}) \to {tpos F ↾}_{((V \times V) \cup \{\emptyset\})} = tpos F$
5	2 3 4	mp2an	$⊢ {tpos F ↾}_{((V \times V) \cup \{\emptyset\})} = tpos F$
6	5	reseq1i	$⊢ {({tpos F ↾}_{((V \times V) \cup \{\emptyset\})}) ↾}_{R} = {tpos F ↾}_{R}$
7		resres	$⊢ {({tpos F ↾}_{R}) ↾}_{((V \times V) \cup \{\emptyset\})} = {tpos F ↾}_{(R \cap ((V \times V) \cup \{\emptyset\}))}$
8	1 6 7	3eqtr3i	$⊢ {tpos F ↾}_{R} = {tpos F ↾}_{(R \cap ((V \times V) \cup \{\emptyset\}))}$
9		indi	$⊢ R \cap ((V \times V) \cup \{\emptyset\}) = (R \cap (V \times V)) \cup (R \cap \{\emptyset\})$
10		cnvcnv	$⊢ {R^{-1}}^{-1} = R \cap (V \times V)$
11	10	uneq1i	$⊢ {R^{-1}}^{-1} \cup (R \cap \{\emptyset\}) = (R \cap (V \times V)) \cup (R \cap \{\emptyset\})$
12	9 11	eqtr4i	$⊢ R \cap ((V \times V) \cup \{\emptyset\}) = {R^{-1}}^{-1} \cup (R \cap \{\emptyset\})$
13	12	reseq2i	$⊢ {tpos F ↾}_{(R \cap ((V \times V) \cup \{\emptyset\}))} = {tpos F ↾}_{({R^{-1}}^{-1} \cup (R \cap \{\emptyset\}))}$
14		resundi	$⊢ {tpos F ↾}_{({R^{-1}}^{-1} \cup (R \cap \{\emptyset\}))} = ({tpos F ↾}_{{R^{-1}}^{-1}}) \cup ({tpos F ↾}_{(R \cap \{\emptyset\})})$
15		rescom	$⊢ {({tpos F ↾}_{\{\emptyset\}}) ↾}_{R} = {({tpos F ↾}_{R}) ↾}_{\{\emptyset\}}$
16		tposres0	$⊢ {tpos F ↾}_{\{\emptyset\}} = {F ↾}_{\{\emptyset\}}$
17	16	reseq1i	$⊢ {({tpos F ↾}_{\{\emptyset\}}) ↾}_{R} = {({F ↾}_{\{\emptyset\}}) ↾}_{R}$
18		resres	$⊢ {({tpos F ↾}_{R}) ↾}_{\{\emptyset\}} = {tpos F ↾}_{(R \cap \{\emptyset\})}$
19	15 17 18	3eqtr3ri	$⊢ {tpos F ↾}_{(R \cap \{\emptyset\})} = {({F ↾}_{\{\emptyset\}}) ↾}_{R}$
20		rescom	$⊢ {({F ↾}_{\{\emptyset\}}) ↾}_{R} = {({F ↾}_{R}) ↾}_{\{\emptyset\}}$
21		resres	$⊢ {({F ↾}_{R}) ↾}_{\{\emptyset\}} = {F ↾}_{(R \cap \{\emptyset\})}$
22	19 20 21	3eqtri	$⊢ {tpos F ↾}_{(R \cap \{\emptyset\})} = {F ↾}_{(R \cap \{\emptyset\})}$
23	22	uneq2i	$⊢ ({tpos F ↾}_{{R^{-1}}^{-1}}) \cup ({tpos F ↾}_{(R \cap \{\emptyset\})}) = ({tpos F ↾}_{{R^{-1}}^{-1}}) \cup ({F ↾}_{(R \cap \{\emptyset\})})$
24	14 23	eqtri	$⊢ {tpos F ↾}_{({R^{-1}}^{-1} \cup (R \cap \{\emptyset\}))} = ({tpos F ↾}_{{R^{-1}}^{-1}}) \cup ({F ↾}_{(R \cap \{\emptyset\})})$
25	8 13 24	3eqtri	$⊢ {tpos F ↾}_{R} = ({tpos F ↾}_{{R^{-1}}^{-1}}) \cup ({F ↾}_{(R \cap \{\emptyset\})})$

Metamath Proof Explorer

Theorem tposresg

Proof