ttrclexg

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

		Ref	Expression
	Assertion	ttrclexg	$⊢ R \in V \to t++ R \in V$

Step	Hyp	Ref	Expression
1		dmexg	$⊢ R \in V \to dom R \in V$
2		rnexg	$⊢ R \in V \to ran R \in V$
3	1 2	xpexd	$⊢ R \in V \to dom R \times ran R \in V$
4		relttrcl	$⊢ Rel t++ R$
5		relssdmrn	$⊢ Rel t++ R \to t++ R \subseteq dom t++ R \times ran t++ R$
6	4 5	ax-mp	$⊢ t++ R \subseteq dom t++ R \times ran t++ R$
7		dmttrcl	$⊢ dom t++ R = dom R$
8		rnttrcl	$⊢ ran t++ R = ran R$
9	7 8	xpeq12i	$⊢ dom t++ R \times ran t++ R = dom R \times ran R$
10	6 9	sseqtri	$⊢ t++ R \subseteq dom R \times ran R$
11	10	a1i	$⊢ R \in V \to t++ R \subseteq dom R \times ran R$
12	3 11	ssexd	$⊢ R \in V \to t++ R \in V$

Metamath Proof Explorer