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