tposexg

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

		Ref	Expression
	Assertion	tposexg	$⊢ F \in V \to tpos F \in V$

Step	Hyp	Ref	Expression
1		tposssxp	$⊢ tpos F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F$
2		dmexg	$⊢ F \in V \to dom F \in V$
3		cnvexg	$⊢ dom F \in V \to {dom F}^{-1} \in V$
4	2 3	syl	$⊢ F \in V \to {dom F}^{-1} \in V$
5		p0ex	$⊢ \{\emptyset\} \in V$
6		unexg	$⊢ ({dom F}^{-1} \in V \land \{\emptyset\} \in V) \to {dom F}^{-1} \cup \{\emptyset\} \in V$
7	4 5 6	sylancl	$⊢ F \in V \to {dom F}^{-1} \cup \{\emptyset\} \in V$
8		rnexg	$⊢ F \in V \to ran F \in V$
9	7 8	xpexd	$⊢ F \in V \to ({dom F}^{-1} \cup \{\emptyset\}) \times ran F \in V$
10		ssexg	$⊢ (tpos F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F \land ({dom F}^{-1} \cup \{\emptyset\}) \times ran F \in V) \to tpos F \in V$
11	1 9 10	sylancr	$⊢ F \in V \to tpos F \in V$

Metamath Proof Explorer