This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nftpos

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

		Ref	Expression
	Hypothesis	nftpos.1	$⊢ \underline{Ⅎ} x F$
	Assertion	nftpos	$⊢ \underline{Ⅎ} x tpos F$

Step	Hyp	Ref	Expression
1		nftpos.1	$⊢ \underline{Ⅎ} x F$
2		dftpos4	$⊢ tpos F = F \circ (y \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{y\}}^{-1})$
3		nfcv	$⊢ \underline{Ⅎ} x (y \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{y\}}^{-1})$
4	1 3	nfco	$⊢ \underline{Ⅎ} x (F \circ (y \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{y\}}^{-1}))$
5	2 4	nfcxfr	$⊢ \underline{Ⅎ} x tpos F$