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

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 )