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

Metamath Proof Explorer

Theorem dftpos2

Description: Alternate definition of tpos when F has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	dftpos2	⊢ ( Rel dom 𝐹 → tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ^◡ dom 𝐹 ↦ ∪ ^◡ { 𝑥 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmtpos	⊢ ( Rel dom 𝐹 → dom tpos 𝐹 = ^◡ dom 𝐹 )
2	1	reseq2d	⊢ ( Rel dom 𝐹 → ( tpos 𝐹 ↾ dom tpos 𝐹 ) = ( tpos 𝐹 ↾ ^◡ dom 𝐹 ) )
3		reltpos	⊢ Rel tpos 𝐹
4		resdm	⊢ ( Rel tpos 𝐹 → ( tpos 𝐹 ↾ dom tpos 𝐹 ) = tpos 𝐹 )
5	3 4	ax-mp	⊢ ( tpos 𝐹 ↾ dom tpos 𝐹 ) = tpos 𝐹
6		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) )
7	6	reseq1i	⊢ ( tpos 𝐹 ↾ ^◡ dom 𝐹 ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) ↾ ^◡ dom 𝐹 )
8		resco	⊢ ( ( 𝐹 ∘ ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ) ↾ ^◡ dom 𝐹 ) = ( 𝐹 ∘ ( ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ^◡ dom 𝐹 ) )
9		ssun1	⊢ ^◡ dom 𝐹 ⊆ ( ^◡ dom 𝐹 ∪ { ∅ } )
10		resmpt	⊢ ( ^◡ dom 𝐹 ⊆ ( ^◡ dom 𝐹 ∪ { ∅ } ) → ( ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ^◡ dom 𝐹 ) = ( 𝑥 ∈ ^◡ dom 𝐹 ↦ ∪ ^◡ { 𝑥 } ) )
11	9 10	ax-mp	⊢ ( ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ^◡ dom 𝐹 ) = ( 𝑥 ∈ ^◡ dom 𝐹 ↦ ∪ ^◡ { 𝑥 } )
12	11	coeq2i	⊢ ( 𝐹 ∘ ( ( 𝑥 ∈ ( ^◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ^◡ { 𝑥 } ) ↾ ^◡ dom 𝐹 ) ) = ( 𝐹 ∘ ( 𝑥 ∈ ^◡ dom 𝐹 ↦ ∪ ^◡ { 𝑥 } ) )
13	7 8 12	3eqtri	⊢ ( tpos 𝐹 ↾ ^◡ dom 𝐹 ) = ( 𝐹 ∘ ( 𝑥 ∈ ^◡ dom 𝐹 ↦ ∪ ^◡ { 𝑥 } ) )
14	2 5 13	3eqtr3g	⊢ ( Rel dom 𝐹 → tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ^◡ dom 𝐹 ↦ ∪ ^◡ { 𝑥 } ) ) )