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 F = ( ( F o. ( x e. `' dom F |-> U. `' { x } ) ) u. ( { (/) } X. ( F " { (/) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dftpos5	|- tpos F = ( F o. ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } ) )
2		coundi	|- ( F o. ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } ) ) = ( ( F o. ( x e. `' dom F |-> U. `' { x } ) ) u. ( F o. { <. (/) , (/) >. } ) )
3		0ex	|- (/) e. _V
4	3 3	cosni	|- ( F o. { <. (/) , (/) >. } ) = ( { (/) } X. ( F " { (/) } ) )
5	4	uneq2i	|- ( ( F o. ( x e. `' dom F |-> U. `' { x } ) ) u. ( F o. { <. (/) , (/) >. } ) ) = ( ( F o. ( x e. `' dom F |-> U. `' { x } ) ) u. ( { (/) } X. ( F " { (/) } ) ) )
6	1 2 5	3eqtri	|- tpos F = ( ( F o. ( x e. `' dom F |-> U. `' { x } ) ) u. ( { (/) } X. ( F " { (/) } ) ) )