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

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 ( 𝑅 ∈ TosetRel → ◡ 𝑅 ∈ TosetRel )

Proof

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