Theorem nftpos

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

	Ref	Expression
Hypothesis	nftpos.1	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	nftpos	$$⊢\underset{\_}{Ⅎ}xtposF$$

Proof

Step	Hyp	Ref	Expression
1		nftpos.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		dftpos4	$$⊢tposF=F\circ \left(y\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{y\right\}}^{-1}\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(y\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{y\right\}}^{-1}\right)$$
4	1 3	nfco	$$⊢\underset{\_}{Ⅎ}x\left(F\circ \left(y\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{y\right\}}^{-1}\right)\right)$$
5	2 4	nfcxfr	$$⊢\underset{\_}{Ⅎ}xtposF$$