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 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) )