Theorem tposexg

Description: The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	tposexg	⊢ ( 𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		tposssxp	⊢ tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )
2		dmexg	⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
3		cnvexg	⊢ ( dom 𝐹 ∈ V → ◡ dom 𝐹 ∈ V )
4	2 3	syl	⊢ ( 𝐹 ∈ 𝑉 → ◡ dom 𝐹 ∈ V )
5		p0ex	⊢ { ∅ } ∈ V
6		unexg	⊢ ( ( ◡ dom 𝐹 ∈ V ∧ { ∅ } ∈ V ) → ( ◡ dom 𝐹 ∪ { ∅ } ) ∈ V )
7	4 5 6	sylancl	⊢ ( 𝐹 ∈ 𝑉 → ( ◡ dom 𝐹 ∪ { ∅ } ) ∈ V )
8		rnexg	⊢ ( 𝐹 ∈ 𝑉 → ran 𝐹 ∈ V )
9	7 8	xpexd	⊢ ( 𝐹 ∈ 𝑉 → ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) ∈ V )
10		ssexg	⊢ ( ( tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) ∧ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) ∈ V ) → tpos 𝐹 ∈ V )
11	1 9 10	sylancr	⊢ ( 𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V )