Theorem tposssxp

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

	Ref	Expression
Assertion	tposssxp	⊢ tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
2		cossxp	⊢ ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ⊆ ( dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) × ran 𝐹 )
3	1 2	eqsstri	⊢ tpos 𝐹 ⊆ ( dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) × ran 𝐹 )
4		eqid	⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
5	4	dmmptss	⊢ dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ( ◡ dom 𝐹 ∪ { ∅ } )
6		xpss1	⊢ ( dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ⊆ ( ◡ dom 𝐹 ∪ { ∅ } ) → ( dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) × ran 𝐹 ) ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) )
7	5 6	ax-mp	⊢ ( dom ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) × ran 𝐹 ) ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )
8	3 7	sstri	⊢ tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )