Theorem dftpos6

Description: Alternate definition of tpos . The second half of the right hand side could apply ressn and become ` ( F |`{ (/) } ) (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	dftpos6	⊢ tpos 𝐹 = ( ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( { ∅ } × ( 𝐹 “ { ∅ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dftpos5	⊢ tpos 𝐹 = ( 𝐹 ∘ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } ) )
2		coundi	⊢ ( 𝐹 ∘ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } ) ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( 𝐹 ∘ { ⟨ ∅ , ∅ ⟩ } ) )
3		0ex	⊢ ∅ ∈ V
4	3 3	cosni	⊢ ( 𝐹 ∘ { ⟨ ∅ , ∅ ⟩ } ) = ( { ∅ } × ( 𝐹 “ { ∅ } ) )
5	4	uneq2i	⊢ ( ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( 𝐹 ∘ { ⟨ ∅ , ∅ ⟩ } ) ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( { ∅ } × ( 𝐹 “ { ∅ } ) ) )
6	1 2 5	3eqtri	⊢ tpos 𝐹 = ( ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ) ∪ ( { ∅ } × ( 𝐹 “ { ∅ } ) ) )