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

Proof

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