Theorem isps

Description: The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008)

	Ref	Expression
Assertion	isps	⊢ ( 𝑅 ∈ 𝐴 → ( 𝑅 ∈ PosetRel ↔ ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		releq	⊢ ( 𝑟 = 𝑅 → ( Rel 𝑟 ↔ Rel 𝑅 ) )
2		coeq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∘ 𝑟 ) = ( 𝑅 ∘ 𝑟 ) )
3		coeq2	⊢ ( 𝑟 = 𝑅 → ( 𝑅 ∘ 𝑟 ) = ( 𝑅 ∘ 𝑅 ) )
4	2 3	eqtrd	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∘ 𝑟 ) = ( 𝑅 ∘ 𝑅 ) )
5		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
6	4 5	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) )
7		cnveq	⊢ ( 𝑟 = 𝑅 → ◡ 𝑟 = ◡ 𝑅 )
8	5 7	ineq12d	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∩ ◡ 𝑟 ) = ( 𝑅 ∩ ◡ 𝑅 ) )
9		unieq	⊢ ( 𝑟 = 𝑅 → ∪ 𝑟 = ∪ 𝑅 )
10	9	unieqd	⊢ ( 𝑟 = 𝑅 → ∪ ∪ 𝑟 = ∪ ∪ 𝑅 )
11	10	reseq2d	⊢ ( 𝑟 = 𝑅 → ( I ↾ ∪ ∪ 𝑟 ) = ( I ↾ ∪ ∪ 𝑅 ) )
12	8 11	eqeq12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) ↔ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) )
13	1 6 12	3anbi123d	⊢ ( 𝑟 = 𝑅 → ( ( Rel 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) ) ↔ ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) ) )
14		df-ps	⊢ PosetRel = { 𝑟 ∣ ( Rel 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( 𝑟 ∩ ◡ 𝑟 ) = ( I ↾ ∪ ∪ 𝑟 ) ) }
15	13 14	elab2g	⊢ ( 𝑅 ∈ 𝐴 → ( 𝑅 ∈ PosetRel ↔ ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) ) )