Theorem tposss

Description: Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	tposss	$$⊢F\subseteq G\to tposF\subseteq tposG$$

Proof

Step	Hyp	Ref	Expression
1		coss1	$$⊢F\subseteq G\to F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq G\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
2		dmss	$$⊢F\subseteq G\to \mathrm{dom}F\subseteq \mathrm{dom}G$$
3		cnvss	$$⊢\mathrm{dom}F\subseteq \mathrm{dom}G\to {\mathrm{dom}F}^{-1}\subseteq {\mathrm{dom}G}^{-1}$$
4		unss1	$$⊢{\mathrm{dom}F}^{-1}\subseteq {\mathrm{dom}G}^{-1}\to {\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\subseteq {\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}$$
5		resmpt	$$⊢{\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\subseteq {\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\to {\left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)}=\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
6	2 3 4 5	4syl	$$⊢F\subseteq G\to {\left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)}=\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
7		resss	$$⊢{\left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\upharpoonright }_{\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)}\subseteq \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
8	6 7	eqsstrrdi	$$⊢F\subseteq G\to \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
9		coss2	$$⊢\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\to G\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq G\circ \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
10	8 9	syl	$$⊢F\subseteq G\to G\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq G\circ \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
11	1 10	sstrd	$$⊢F\subseteq G\to F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\subseteq G\circ \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
12		df-tpos	$$⊢tposF=F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
13		df-tpos	$$⊢tposG=G\circ \left(x\in \left({\mathrm{dom}G}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
14	11 12 13	3sstr4g	$$⊢F\subseteq G\to tposF\subseteq tposG$$