# Metamath Proof Explorer

## Theorem cnvtsr

Description: The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion cnvtsr $⊢ R ∈ TosetRel → R -1 ∈ TosetRel$

### Proof

Step Hyp Ref Expression
1 tsrps $⊢ R ∈ TosetRel → R ∈ PosetRel$
2 cnvps $⊢ R ∈ PosetRel → R -1 ∈ PosetRel$
3 1 2 syl $⊢ R ∈ TosetRel → R -1 ∈ PosetRel$
4 eqid $⊢ dom ⁡ R = dom ⁡ R$
5 4 istsr $⊢ R ∈ TosetRel ↔ R ∈ PosetRel ∧ dom ⁡ R × dom ⁡ R ⊆ R ∪ R -1$
6 5 simprbi $⊢ R ∈ TosetRel → dom ⁡ R × dom ⁡ R ⊆ R ∪ R -1$
7 4 psrn $⊢ R ∈ PosetRel → dom ⁡ R = ran ⁡ R$
8 1 7 syl $⊢ R ∈ TosetRel → dom ⁡ R = ran ⁡ R$
9 8 sqxpeqd $⊢ R ∈ TosetRel → dom ⁡ R × dom ⁡ R = ran ⁡ R × ran ⁡ R$
10 psrel $⊢ R ∈ PosetRel → Rel ⁡ R$
11 1 10 syl $⊢ R ∈ TosetRel → Rel ⁡ R$
12 dfrel2 $⊢ Rel ⁡ R ↔ R -1 -1 = R$
13 11 12 sylib $⊢ R ∈ TosetRel → R -1 -1 = R$
14 13 uneq2d $⊢ R ∈ TosetRel → R -1 ∪ R -1 -1 = R -1 ∪ R$
15 uncom $⊢ R -1 ∪ R = R ∪ R -1$
16 14 15 eqtr2di $⊢ R ∈ TosetRel → R ∪ R -1 = R -1 ∪ R -1 -1$
17 6 9 16 3sstr3d $⊢ R ∈ TosetRel → ran ⁡ R × ran ⁡ R ⊆ R -1 ∪ R -1 -1$
18 df-rn $⊢ ran ⁡ R = dom ⁡ R -1$
19 18 istsr $⊢ R -1 ∈ TosetRel ↔ R -1 ∈ PosetRel ∧ ran ⁡ R × ran ⁡ R ⊆ R -1 ∪ R -1 -1$
20 3 17 19 sylanbrc $⊢ R ∈ TosetRel → R -1 ∈ TosetRel$