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 )