Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Partial and total orderings
po2ne
Next ⟩
po0
Metamath Proof Explorer
Ascii
Unicode
Theorem
po2ne
Description:
Two sets related by a partial order are not equal.
(Contributed by
AV
, 13-Mar-2023)
Ref
Expression
Assertion
po2ne
⊢
R
Po
V
∧
A
∈
V
∧
B
∈
V
∧
A
R
B
→
A
≠
B
Proof
Step
Hyp
Ref
Expression
1
breq1
⊢
A
=
B
→
A
R
B
↔
B
R
B
2
poirr
⊢
R
Po
V
∧
B
∈
V
→
¬
B
R
B
3
2
adantrl
⊢
R
Po
V
∧
A
∈
V
∧
B
∈
V
→
¬
B
R
B
4
3
pm2.21d
⊢
R
Po
V
∧
A
∈
V
∧
B
∈
V
→
B
R
B
→
A
≠
B
5
4
ex
⊢
R
Po
V
→
A
∈
V
∧
B
∈
V
→
B
R
B
→
A
≠
B
6
5
com13
⊢
B
R
B
→
A
∈
V
∧
B
∈
V
→
R
Po
V
→
A
≠
B
7
1
6
syl6bi
⊢
A
=
B
→
A
R
B
→
A
∈
V
∧
B
∈
V
→
R
Po
V
→
A
≠
B
8
7
com24
⊢
A
=
B
→
R
Po
V
→
A
∈
V
∧
B
∈
V
→
A
R
B
→
A
≠
B
9
8
3impd
⊢
A
=
B
→
R
Po
V
∧
A
∈
V
∧
B
∈
V
∧
A
R
B
→
A
≠
B
10
ax-1
⊢
A
≠
B
→
R
Po
V
∧
A
∈
V
∧
B
∈
V
∧
A
R
B
→
A
≠
B
11
9
10
pm2.61ine
⊢
R
Po
V
∧
A
∈
V
∧
B
∈
V
∧
A
R
B
→
A
≠
B