![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > psrel | Structured version Visualization version GIF version |
Description: A poset is a relation. (Contributed by NM, 12-May-2008.) |
Ref | Expression |
---|---|
psrel | ⊢ (𝐴 ∈ PosetRel → Rel 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isps 17514 | . . 3 ⊢ (𝐴 ∈ PosetRel → (𝐴 ∈ PosetRel ↔ (Rel 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴 ∧ (𝐴 ∩ ◡𝐴) = ( I ↾ ∪ ∪ 𝐴)))) | |
2 | 1 | ibi 259 | . 2 ⊢ (𝐴 ∈ PosetRel → (Rel 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴 ∧ (𝐴 ∩ ◡𝐴) = ( I ↾ ∪ ∪ 𝐴))) |
3 | 2 | simp1d 1173 | 1 ⊢ (𝐴 ∈ PosetRel → Rel 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ∩ cin 3766 ⊆ wss 3767 ∪ cuni 4626 I cid 5217 ◡ccnv 5309 ↾ cres 5312 ∘ ccom 5314 Rel wrel 5315 PosetRelcps 17510 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-rex 3093 df-v 3385 df-in 3774 df-ss 3781 df-uni 4627 df-br 4842 df-opab 4904 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-res 5322 df-ps 17512 |
This theorem is referenced by: pslem 17518 cnvps 17524 psss 17526 cnvtsr 17534 tsrdir 17550 |
Copyright terms: Public domain | W3C validator |