Metamath Proof Explorer

Theorem rtrclexlem

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

Ref Expression
Assertion rtrclexlem 
|- ( R e. V -> ( R u. ( ( dom R u. ran R ) X. ( dom R u. 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 unexg 
 |-  ( ( dom R e. _V /\ ran R e. _V ) -> ( dom R u. ran R ) e. _V )
4 1 2 3 syl2anc 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
5 sqxpexg 
 |-  ( ( dom R u. ran R ) e. _V -> ( ( dom R u. ran R ) X. ( dom R u. ran R ) ) e. _V )
6 4 5 syl 
 |-  ( R e. V -> ( ( dom R u. ran R ) X. ( dom R u. ran R ) ) e. _V )
7 unexg 
 |-  ( ( R e. V /\ ( ( dom R u. ran R ) X. ( dom R u. ran R ) ) e. _V ) -> ( R u. ( ( dom R u. ran R ) X. ( dom R u. ran R ) ) ) e. _V )
8 6 7 mpdan 
 |-  ( R e. V -> ( R u. ( ( dom R u. ran R ) X. ( dom R u. ran R ) ) ) e. _V )