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