Metamath Proof Explorer

Theorem tposss

Description: Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion tposss ⊢ F ⊆ G → tpos F ⊆ tpos G

Proof

Step Hyp Ref Expression
1 coss1 ⊢ F ⊆ G → F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ G ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
2 dmss ⊢ F ⊆ G → dom ⁡ F ⊆ dom ⁡ G
3 cnvss ⊢ dom ⁡ F ⊆ dom ⁡ G → dom ⁡ F -1 ⊆ dom ⁡ G -1
4 unss1 ⊢ dom ⁡ F -1 ⊆ dom ⁡ G -1 → dom ⁡ F -1 ∪ ∅ ⊆ dom ⁡ G -1 ∪ ∅
5 resmpt ⊢ dom ⁡ F -1 ∪ ∅ ⊆ dom ⁡ G -1 ∪ ∅ → x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1 ↾ dom ⁡ F -1 ∪ ∅ = x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
6 2 3 4 5 4syl ⊢ F ⊆ G → x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1 ↾ dom ⁡ F -1 ∪ ∅ = x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
7 resss ⊢ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1 ↾ dom ⁡ F -1 ∪ ∅ ⊆ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1
8 6 7 eqsstrrdi ⊢ F ⊆ G → x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1
9 coss2 ⊢ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1 → G ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ G ∘ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1
10 8 9 syl ⊢ F ⊆ G → G ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ G ∘ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1
11 1 10 sstrd ⊢ F ⊆ G → F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1 ⊆ G ∘ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1
12 df-tpos ⊢ tpos F = F ∘ x ∈ dom ⁡ F -1 ∪ ∅ ⟼ ⋃ x -1
13 df-tpos ⊢ tpos G = G ∘ x ∈ dom ⁡ G -1 ∪ ∅ ⟼ ⋃ x -1
14 11 12 13 3sstr4g ⊢ F ⊆ G → tpos F ⊆ tpos G