Metamath Proof Explorer


Theorem cnvps

Description: The converse of a poset is a poset. In the general case (`' R e. PosetRel -> R e. PosetRel ) ` is not true. See cnvpsb for a special case where the property holds. (Contributed by FL, 5-Jan-2009) (Proof shortened by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion cnvps ( 𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel )

Proof

Step Hyp Ref Expression
1 relcnv Rel 𝑅
2 1 a1i ( 𝑅 ∈ PosetRel → Rel 𝑅 )
3 cnvco ( 𝑅𝑅 ) = ( 𝑅 𝑅 )
4 pstr2 ( 𝑅 ∈ PosetRel → ( 𝑅𝑅 ) ⊆ 𝑅 )
5 cnvss ( ( 𝑅𝑅 ) ⊆ 𝑅 ( 𝑅𝑅 ) ⊆ 𝑅 )
6 4 5 syl ( 𝑅 ∈ PosetRel → ( 𝑅𝑅 ) ⊆ 𝑅 )
7 3 6 eqsstrrid ( 𝑅 ∈ PosetRel → ( 𝑅 𝑅 ) ⊆ 𝑅 )
8 psrel ( 𝑅 ∈ PosetRel → Rel 𝑅 )
9 dfrel2 ( Rel 𝑅 𝑅 = 𝑅 )
10 8 9 sylib ( 𝑅 ∈ PosetRel → 𝑅 = 𝑅 )
11 10 ineq2d ( 𝑅 ∈ PosetRel → ( 𝑅 𝑅 ) = ( 𝑅𝑅 ) )
12 incom ( 𝑅𝑅 ) = ( 𝑅 𝑅 )
13 11 12 eqtrdi ( 𝑅 ∈ PosetRel → ( 𝑅 𝑅 ) = ( 𝑅 𝑅 ) )
14 psref2 ( 𝑅 ∈ PosetRel → ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) )
15 relcnvfld ( Rel 𝑅 𝑅 = 𝑅 )
16 8 15 syl ( 𝑅 ∈ PosetRel → 𝑅 = 𝑅 )
17 16 reseq2d ( 𝑅 ∈ PosetRel → ( I ↾ 𝑅 ) = ( I ↾ 𝑅 ) )
18 13 14 17 3eqtrd ( 𝑅 ∈ PosetRel → ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) )
19 cnvexg ( 𝑅 ∈ PosetRel → 𝑅 ∈ V )
20 isps ( 𝑅 ∈ V → ( 𝑅 ∈ PosetRel ↔ ( Rel 𝑅 ∧ ( 𝑅 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) ) ) )
21 19 20 syl ( 𝑅 ∈ PosetRel → ( 𝑅 ∈ PosetRel ↔ ( Rel 𝑅 ∧ ( 𝑅 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) ) ) )
22 2 7 18 21 mpbir3and ( 𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel )