Theorem dftpos5

Description: Alternate definition of tpos . (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	dftpos5	⊢ tpos 𝐹 = ( 𝐹 ∘ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		df-tpos	⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
2		mptun	⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ ( 𝑥 ∈ { ∅ } ↦ ∪ ◡ { 𝑥 } ) )
3		0ex	⊢ ∅ ∈ V
4		sneq	⊢ ( 𝑥 = ∅ → { 𝑥 } = { ∅ } )
5	4	cnveqd	⊢ ( 𝑥 = ∅ → ◡ { 𝑥 } = ◡ { ∅ } )
6	5	unieqd	⊢ ( 𝑥 = ∅ → ∪ ◡ { 𝑥 } = ∪ ◡ { ∅ } )
7		cnvsn0	⊢ ◡ { ∅ } = ∅
8	7	unieqi	⊢ ∪ ◡ { ∅ } = ∪ ∅
9		uni0	⊢ ∪ ∅ = ∅
10	8 9	eqtri	⊢ ∪ ◡ { ∅ } = ∅
11	6 10	eqtrdi	⊢ ( 𝑥 = ∅ → ∪ ◡ { 𝑥 } = ∅ )
12	11	fmptsng	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → { ⟨ ∅ , ∅ ⟩ } = ( 𝑥 ∈ { ∅ } ↦ ∪ ◡ { 𝑥 } ) )
13	3 3 12	mp2an	⊢ { ⟨ ∅ , ∅ ⟩ } = ( 𝑥 ∈ { ∅ } ↦ ∪ ◡ { 𝑥 } )
14	13	uneq2i	⊢ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } ) = ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ ( 𝑥 ∈ { ∅ } ↦ ∪ ◡ { 𝑥 } ) )
15	2 14	eqtr4i	⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) = ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } )
16	15	coeq2i	⊢ ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) = ( 𝐹 ∘ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } ) )
17	1 16	eqtri	⊢ tpos 𝐹 = ( 𝐹 ∘ ( ( 𝑥 ∈ ◡ dom 𝐹 ↦ ∪ ◡ { 𝑥 } ) ∪ { ⟨ ∅ , ∅ ⟩ } ) )