Theorem nftpos

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

	Ref	Expression
Hypothesis	nftpos.1	⊢ Ⅎ 𝑥 𝐹
Assertion	nftpos	⊢ Ⅎ 𝑥 tpos 𝐹

Proof

Step	Hyp	Ref	Expression
1		nftpos.1	⊢ Ⅎ 𝑥 𝐹
2		dftpos4	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑦 } ) )
3		nfcv	⊢ Ⅎ 𝑥 ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑦 } )
4	1 3	nfco	⊢ Ⅎ 𝑥 ( 𝐹 ∘ ( 𝑦 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑦 } ) )
5	2 4	nfcxfr	⊢ Ⅎ 𝑥 tpos 𝐹