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 ∈ V → R ∪ dom ⁡ R ∪ ran ⁡ 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 unexd ⊢ R ∈ V → dom ⁡ R ∪ ran ⁡ R ∈ V
4 sqxpexg ⊢ dom ⁡ R ∪ ran ⁡ R ∈ V → dom ⁡ R ∪ ran ⁡ R × dom ⁡ R ∪ ran ⁡ R ∈ V
5 3 4 syl ⊢ R ∈ V → dom ⁡ R ∪ ran ⁡ R × dom ⁡ R ∪ ran ⁡ R ∈ V
6 unexg ⊢ R ∈ V ∧ dom ⁡ R ∪ ran ⁡ R × dom ⁡ R ∪ ran ⁡ R ∈ V → R ∪ dom ⁡ R ∪ ran ⁡ R × dom ⁡ R ∪ ran ⁡ R ∈ V
7 5 6 mpdan ⊢ R ∈ V → R ∪ dom ⁡ R ∪ ran ⁡ R × dom ⁡ R ∪ ran ⁡ R ∈ V