This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )