Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Partial and total orderings
po2nr
Next ⟩
po3nr
Metamath Proof Explorer
Ascii
Unicode
Theorem
po2nr
Description:
A partial order has no 2-cycle loops.
(Contributed by
NM
, 27-Mar-1997)
Ref
Expression
Assertion
po2nr
⊢
R
Po
A
∧
B
∈
A
∧
C
∈
A
→
¬
B
R
C
∧
C
R
B
Proof
Step
Hyp
Ref
Expression
1
poirr
⊢
R
Po
A
∧
B
∈
A
→
¬
B
R
B
2
1
adantrr
⊢
R
Po
A
∧
B
∈
A
∧
C
∈
A
→
¬
B
R
B
3
potr
⊢
R
Po
A
∧
B
∈
A
∧
C
∈
A
∧
B
∈
A
→
B
R
C
∧
C
R
B
→
B
R
B
4
3
3exp2
⊢
R
Po
A
→
B
∈
A
→
C
∈
A
→
B
∈
A
→
B
R
C
∧
C
R
B
→
B
R
B
5
4
com34
⊢
R
Po
A
→
B
∈
A
→
B
∈
A
→
C
∈
A
→
B
R
C
∧
C
R
B
→
B
R
B
6
5
pm2.43d
⊢
R
Po
A
→
B
∈
A
→
C
∈
A
→
B
R
C
∧
C
R
B
→
B
R
B
7
6
imp32
⊢
R
Po
A
∧
B
∈
A
∧
C
∈
A
→
B
R
C
∧
C
R
B
→
B
R
B
8
2
7
mtod
⊢
R
Po
A
∧
B
∈
A
∧
C
∈
A
→
¬
B
R
C
∧
C
R
B