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