Metamath Proof Explorer

Theorem dmtposss

Description: The domain of tpos F is a subset. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion dmtposss 
|- dom tpos F C_ ( ( _V X. _V ) u. { (/) } )

Proof

Step Hyp Ref Expression
1 df-tpos 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
2 1 dmeqi 
 |-  dom tpos F = dom ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
3 dmcoss 
 |-  dom ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
4 eqid 
 |-  ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
5 4 dmmptss 
 |-  dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( `' dom F u. { (/) } )
6 relcnv 
 |-  Rel `' dom F
7 df-rel 
 |-  ( Rel `' dom F <-> `' dom F C_ ( _V X. _V ) )
8 6 7 mpbi 
 |-  `' dom F C_ ( _V X. _V )
9 unss1 
 |-  ( `' dom F C_ ( _V X. _V ) -> ( `' dom F u. { (/) } ) C_ ( ( _V X. _V ) u. { (/) } ) )
10 8 9 ax-mp 
 |-  ( `' dom F u. { (/) } ) C_ ( ( _V X. _V ) u. { (/) } )
11 5 10 sstri 
 |-  dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( ( _V X. _V ) u. { (/) } )
12 3 11 sstri 
 |-  dom ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( ( _V X. _V ) u. { (/) } )
13 2 12 eqsstri 
 |-  dom tpos F C_ ( ( _V X. _V ) u. { (/) } )