Theorem ttrclexg

Description: If R is a set, then so is t++ R . (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Assertion	ttrclexg	⊢ ( 𝑅 ∈ 𝑉 → t++ 𝑅 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dmexg	⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
2		rnexg	⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ∈ V )
3	1 2	xpexd	⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 × ran 𝑅 ) ∈ V )
4		relttrcl	⊢ Rel t++ 𝑅
5		relssdmrn	⊢ ( Rel t++ 𝑅 → t++ 𝑅 ⊆ ( dom t++ 𝑅 × ran t++ 𝑅 ) )
6	4 5	ax-mp	⊢ t++ 𝑅 ⊆ ( dom t++ 𝑅 × ran t++ 𝑅 )
7		dmttrcl	⊢ dom t++ 𝑅 = dom 𝑅
8		rnttrcl	⊢ ran t++ 𝑅 = ran 𝑅
9	7 8	xpeq12i	⊢ ( dom t++ 𝑅 × ran t++ 𝑅 ) = ( dom 𝑅 × ran 𝑅 )
10	6 9	sseqtri	⊢ t++ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 )
11	10	a1i	⊢ ( 𝑅 ∈ 𝑉 → t++ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
12	3 11	ssexd	⊢ ( 𝑅 ∈ 𝑉 → t++ 𝑅 ∈ V )