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 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