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	$$⊢tposF=\left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(\left\{\varnothing \right\}\times F\left[\left\{\varnothing \right\}\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		dftpos5	$$⊢tposF=F\circ \left(\left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\cup \left\{⟨\varnothing ,\varnothing ⟩\right\}\right)$$
2		coundi	$$⊢F\circ \left(\left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\cup \left\{⟨\varnothing ,\varnothing ⟩\right\}\right)=\left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(F\circ \left\{⟨\varnothing ,\varnothing ⟩\right\}\right)$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	3 3	cosni	$$⊢F\circ \left\{⟨\varnothing ,\varnothing ⟩\right\}=\left\{\varnothing \right\}\times F\left[\left\{\varnothing \right\}\right]$$
5	4	uneq2i	$$⊢\left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(F\circ \left\{⟨\varnothing ,\varnothing ⟩\right\}\right)=\left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(\left\{\varnothing \right\}\times F\left[\left\{\varnothing \right\}\right]\right)$$
6	1 2 5	3eqtri	$$⊢tposF=\left(F\circ \left(x\in {\mathrm{dom}F}^{-1}⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\cup \left(\left\{\varnothing \right\}\times F\left[\left\{\varnothing \right\}\right]\right)$$