Metamath Proof Explorer

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 e. V /\ B e. 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 e. V ) -> -. B R B )
3 2 adantrl 
 |-  ( ( R Po V /\ ( A e. V /\ B e. V ) ) -> -. B R B )
4 3 pm2.21d 
 |-  ( ( R Po V /\ ( A e. V /\ B e. V ) ) -> ( B R B -> A =/= B ) )
5 4 ex 
 |-  ( R Po V -> ( ( A e. V /\ B e. V ) -> ( B R B -> A =/= B ) ) )
6 5 com13 
 |-  ( B R B -> ( ( A e. V /\ B e. V ) -> ( R Po V -> A =/= B ) ) )
7 1 6 syl6bi 
 |-  ( A = B -> ( A R B -> ( ( A e. V /\ B e. V ) -> ( R Po V -> A =/= B ) ) ) )
8 7 com24 
 |-  ( A = B -> ( R Po V -> ( ( A e. V /\ B e. V ) -> ( A R B -> A =/= B ) ) ) )
9 8 3impd 
 |-  ( A = B -> ( ( R Po V /\ ( A e. V /\ B e. V ) /\ A R B ) -> A =/= B ) )
10 ax-1 
 |-  ( A =/= B -> ( ( R Po V /\ ( A e. V /\ B e. V ) /\ A R B ) -> A =/= B ) )
11 9 10 pm2.61ine 
 |-  ( ( R Po V /\ ( A e. V /\ B e. V ) /\ A R B ) -> A =/= B )