# Metamath Proof Explorer

## Theorem po2ne

Description: Two classes which are in a partial order relation are not equal. (Contributed by AV, 13-Mar-2023)

Ref Expression
Assertion po2ne ${⊢}\left({R}\mathrm{Po}{V}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\wedge {A}{R}{B}\right)\to {A}\ne {B}$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{A}={B}\to \left({A}{R}{B}↔{B}{R}{B}\right)$
2 poirr ${⊢}\left({R}\mathrm{Po}{V}\wedge {B}\in {V}\right)\to ¬{B}{R}{B}$
3 2 adantrl ${⊢}\left({R}\mathrm{Po}{V}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to ¬{B}{R}{B}$
4 3 pm2.21d ${⊢}\left({R}\mathrm{Po}{V}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \left({B}{R}{B}\to {A}\ne {B}\right)$
5 4 ex ${⊢}{R}\mathrm{Po}{V}\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\to \left({B}{R}{B}\to {A}\ne {B}\right)\right)$
6 5 com13 ${⊢}{B}{R}{B}\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\to \left({R}\mathrm{Po}{V}\to {A}\ne {B}\right)\right)$
7 1 6 syl6bi ${⊢}{A}={B}\to \left({A}{R}{B}\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\to \left({R}\mathrm{Po}{V}\to {A}\ne {B}\right)\right)\right)$
8 7 com24 ${⊢}{A}={B}\to \left({R}\mathrm{Po}{V}\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\to \left({A}{R}{B}\to {A}\ne {B}\right)\right)\right)$
9 8 3impd ${⊢}{A}={B}\to \left(\left({R}\mathrm{Po}{V}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\wedge {A}{R}{B}\right)\to {A}\ne {B}\right)$
10 ax-1 ${⊢}{A}\ne {B}\to \left(\left({R}\mathrm{Po}{V}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\wedge {A}{R}{B}\right)\to {A}\ne {B}\right)$
11 9 10 pm2.61ine ${⊢}\left({R}\mathrm{Po}{V}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\wedge {A}{R}{B}\right)\to {A}\ne {B}$