This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 )