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

Metamath Proof Explorer

Theorem tposss

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

		Ref	Expression
	Assertion	tposss	⊢ ( 𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		coss1	⊢ ( 𝐹 ⊆ 𝐺 → ( 𝐹 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) ⊆ ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) )
2		dmss	⊢ ( 𝐹 ⊆ 𝐺 → dom 𝐹 ⊆ dom 𝐺 )
3		cnvss	⊢ ( dom 𝐹 ⊆ dom 𝐺 → ^◡ dom 𝐹 ⊆ ^◡ dom 𝐺 )
4		unss1	⊢ ( ^◡ dom 𝐹 ⊆ ^◡ dom 𝐺 → ( ^◡ dom 𝐹 ∪ { ∅ } ) ⊆ ( ^◡ dom 𝐺 ∪ { ∅ } ) )
5		resmpt	⊢ ( ( ^◡ dom 𝐹 ∪ { ∅ } ) ⊆ ( ^◡ dom 𝐺 ∪ { ∅ } ) → ( ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ( ^◡ dom 𝐹 ∪ { ∅ } ) ) = ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) )
6	2 3 4 5	4syl	⊢ ( 𝐹 ⊆ 𝐺 → ( ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ( ^◡ dom 𝐹 ∪ { ∅ } ) ) = ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) )
7		resss	⊢ ( ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ( ^◡ dom 𝐹 ∪ { ∅ } ) ) ⊆ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } )
8	6 7	eqsstrrdi	⊢ ( 𝐹 ⊆ 𝐺 → ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ⊆ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) )
9		coss2	⊢ ( ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ⊆ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) → ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) ⊆ ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) )
10	8 9	syl	⊢ ( 𝐹 ⊆ 𝐺 → ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) ⊆ ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) )
11	1 10	sstrd	⊢ ( 𝐹 ⊆ 𝐺 → ( 𝐹 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) ⊆ ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) )
12		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) )
13		df-tpos	⊢ tpos 𝐺 = ( 𝐺 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐺 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) )
14	11 12 13	3sstr4g	⊢ ( 𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺 )