Metamath Proof Explorer

Theorem dftpos5

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

Ref Expression
Assertion dftpos5 
|- tpos F = ( F o. ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } ) )

Proof

Step Hyp Ref Expression
1 df-tpos 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
2 mptun 
 |-  ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( ( x e. `' dom F |-> U. `' { x } ) u. ( x e. { (/) } |-> U. `' { x } ) )
3 0ex 
 |-  (/) e. _V
4 sneq 
 |-  ( x = (/) -> { x } = { (/) } )
5 4 cnveqd 
 |-  ( x = (/) -> `' { x } = `' { (/) } )
6 5 unieqd 
 |-  ( x = (/) -> U. `' { x } = U. `' { (/) } )
7 cnvsn0 
 |-  `' { (/) } = (/)
8 7 unieqi 
 |-  U. `' { (/) } = U. (/)
9 uni0 
 |-  U. (/) = (/)
10 8 9 eqtri 
 |-  U. `' { (/) } = (/)
11 6 10 eqtrdi 
 |-  ( x = (/) -> U. `' { x } = (/) )
12 11 fmptsng 
 |-  ( ( (/) e. _V /\ (/) e. _V ) -> { <. (/) , (/) >. } = ( x e. { (/) } |-> U. `' { x } ) )
13 3 3 12 mp2an 
 |-  { <. (/) , (/) >. } = ( x e. { (/) } |-> U. `' { x } )
14 13 uneq2i 
 |-  ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } ) = ( ( x e. `' dom F |-> U. `' { x } ) u. ( x e. { (/) } |-> U. `' { x } ) )
15 2 14 eqtr4i 
 |-  ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } )
16 15 coeq2i 
 |-  ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) = ( F o. ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } ) )
17 1 16 eqtri 
 |-  tpos F = ( F o. ( ( x e. `' dom F |-> U. `' { x } ) u. { <. (/) , (/) >. } ) )