Metamath Proof Explorer

Theorem ttrclexg

Description: If R is a set, then so is t++ R . (Contributed by Scott Fenton, 26-Oct-2024)

Ref Expression
Assertion ttrclexg 
|- ( R e. V -> t++ R e. _V )

Proof

Step Hyp Ref Expression
1 dmexg 
 |-  ( R e. V -> dom R e. _V )
2 rnexg 
 |-  ( R e. V -> ran R e. _V )
3 1 2 xpexd 
 |-  ( R e. V -> ( dom R X. ran R ) e. _V )
4 relttrcl 
 |-  Rel t++ R
5 relssdmrn 
 |-  ( Rel t++ R -> t++ R C_ ( dom t++ R X. ran t++ R ) )
6 4 5 ax-mp 
 |-  t++ R C_ ( dom t++ R X. ran t++ R )
7 dmttrcl 
 |-  dom t++ R = dom R
8 rnttrcl 
 |-  ran t++ R = ran R
9 7 8 xpeq12i 
 |-  ( dom t++ R X. ran t++ R ) = ( dom R X. ran R )
10 6 9 sseqtri 
 |-  t++ R C_ ( dom R X. ran R )
11 10 a1i 
 |-  ( R e. V -> t++ R C_ ( dom R X. ran R ) )
12 3 11 ssexd 
 |-  ( R e. V -> t++ R e. _V )