Metamath Proof Explorer


Theorem trclexlem

Description: Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 5-May-2020)

Ref Expression
Assertion trclexlem
|- ( R e. V -> ( R u. ( dom R X. ran 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 unexg
 |-  ( ( R e. V /\ ( dom R X. ran R ) e. _V ) -> ( R u. ( dom R X. ran R ) ) e. _V )
5 3 4 mpdan
 |-  ( R e. V -> ( R u. ( dom R X. ran R ) ) e. _V )