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 F ⊆ dom ⁡ F -1 ∪ ∅ × ran ⁡ F

Proof

Step Hyp Ref Expression
1 df-tpos ⊢ tpos F = F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
2 cossxp ⊢ F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 × ran ⁡ F
3 1 2 eqsstri ⊢ tpos F ⊆ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 × ran ⁡ F
4 eqid ⊢ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 = x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
5 4 dmmptss ⊢ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ dom ⁡ F -1 ∪ ∅
6 xpss1 ⊢ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ dom ⁡ F -1 ∪ ∅ → dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 × ran ⁡ F ⊆ dom ⁡ F -1 ∪ ∅ × ran ⁡ F
7 5 6 ax-mp ⊢ dom ⁡ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 × ran ⁡ F ⊆ dom ⁡ F -1 ∪ ∅ × ran ⁡ F
8 3 7 sstri ⊢ tpos F ⊆ dom ⁡ F -1 ∪ ∅ × ran ⁡ F