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 ) |
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 ) |