tposssxp

Description: The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017)

		Ref	Expression
	Assertion	tposssxp	$⊢ tpos F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F$

Step	Hyp	Ref	Expression
1		df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
2		cossxp	$⊢ F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \times ran F$
3	1 2	eqsstri	$⊢ tpos F \subseteq dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \times ran F$
4		eqid	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
5	4	dmmptss	$⊢ dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq {dom F}^{-1} \cup \{\emptyset\}$
6		xpss1	$⊢ dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq {dom F}^{-1} \cup \{\emptyset\} \to dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \times ran F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F$
7	5 6	ax-mp	$⊢ dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \times ran F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F$
8	3 7	sstri	$⊢ tpos F \subseteq ({dom F}^{-1} \cup \{\emptyset\}) \times ran F$

Metamath Proof Explorer