Theorem ttrclexg

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

	Ref	Expression
Assertion	ttrclexg	Could not format assertion : No typesetting found for |- ( R e. V -> t++ R e. _V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dmexg	$$⊢R\in V\to \mathrm{dom}R\in \mathrm{V}$$
2		rnexg	$$⊢R\in V\to \mathrm{ran}R\in \mathrm{V}$$
3	1 2	xpexd	$$⊢R\in V\to \mathrm{dom}R\times \mathrm{ran}R\in \mathrm{V}$$
4		relttrcl	Could not format Rel t++ R : No typesetting found for |- Rel t++ R with typecode |-
5		relssdmrn	Could not format ( Rel t++ R -> t++ R C_ ( dom t++ R X. ran t++ R ) ) : No typesetting found for |- ( Rel t++ R -> t++ R C_ ( dom t++ R X. ran t++ R ) ) with typecode |-
6	4 5	ax-mp	Could not format t++ R C_ ( dom t++ R X. ran t++ R ) : No typesetting found for |- t++ R C_ ( dom t++ R X. ran t++ R ) with typecode |-
7		dmttrcl	Could not format dom t++ R = dom R : No typesetting found for |- dom t++ R = dom R with typecode |-
8		rnttrcl	Could not format ran t++ R = ran R : No typesetting found for |- ran t++ R = ran R with typecode |-
9	7 8	xpeq12i	Could not format ( dom t++ R X. ran t++ R ) = ( dom R X. ran R ) : No typesetting found for |- ( dom t++ R X. ran t++ R ) = ( dom R X. ran R ) with typecode |-
10	6 9	sseqtri	Could not format t++ R C_ ( dom R X. ran R ) : No typesetting found for |- t++ R C_ ( dom R X. ran R ) with typecode |-
11	10	a1i	Could not format ( R e. V -> t++ R C_ ( dom R X. ran R ) ) : No typesetting found for |- ( R e. V -> t++ R C_ ( dom R X. ran R ) ) with typecode |-
12	3 11	ssexd	Could not format ( R e. V -> t++ R e. _V ) : No typesetting found for |- ( R e. V -> t++ R e. _V ) with typecode |-