![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > potr | Structured version Visualization version GIF version |
Description: A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
Ref | Expression |
---|---|
potr | ⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pocl 5445 | . . 3 ⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | |
2 | 1 | imp 410 | . 2 ⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))) |
3 | 2 | simprd 499 | 1 ⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∧ w3a 1084 ∈ wcel 2111 class class class wbr 5030 Po wpo 5436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-v 3443 df-un 3886 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-po 5438 |
This theorem is referenced by: po2nr 5451 po3nr 5452 pofun 5455 sotr 5461 poltletr 5959 predpo 6134 poxp 7805 frfi 8747 wemaplem2 8995 sornom 9688 zorn2lem7 9913 pospo 17575 pocnv 33112 frpomin 33191 poseq 33208 fprlem2 33251 seqpo 35185 |
Copyright terms: Public domain | W3C validator |