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	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( ( dom 𝑅 ∪ ran 𝑅 ) × ( dom 𝑅 ∪ ran 𝑅 ) ) ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dmexg	⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
2		rnexg	⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ∈ V )
3	1 2	unexd	⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
4		sqxpexg	⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) ∈ V → ( ( dom 𝑅 ∪ ran 𝑅 ) × ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
5	3 4	syl	⊢ ( 𝑅 ∈ 𝑉 → ( ( dom 𝑅 ∪ ran 𝑅 ) × ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
6		unexg	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( dom 𝑅 ∪ ran 𝑅 ) × ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V ) → ( 𝑅 ∪ ( ( dom 𝑅 ∪ ran 𝑅 ) × ( dom 𝑅 ∪ ran 𝑅 ) ) ) ∈ V )
7	5 6	mpdan	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( ( dom 𝑅 ∪ ran 𝑅 ) × ( dom 𝑅 ∪ ran 𝑅 ) ) ) ∈ V )