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