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 ∈ V → R ∪ dom ⁡ R × ran ⁡ R ∈ V

Proof

Step Hyp Ref Expression
1 dmexg ⊢ R ∈ V → dom ⁡ R ∈ V
2 rnexg ⊢ R ∈ V → ran ⁡ R ∈ V
3 1 2 xpexd ⊢ R ∈ V → dom ⁡ R × ran ⁡ R ∈ V
4 unexg ⊢ R ∈ V ∧ dom ⁡ R × ran ⁡ R ∈ V → R ∪ dom ⁡ R × ran ⁡ R ∈ V
5 3 4 mpdan ⊢ R ∈ V → R ∪ dom ⁡ R × ran ⁡ R ∈ V