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

Metamath Proof Explorer

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 ↾ ∪ ∪ 𝑅 ) ) ) )