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 ⊢ R ∈ V → t++ R ∈ V

Proof

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