This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐵 ) )
2 poirr ⊢ ( ( 𝑅 Po 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ¬ 𝐵 𝑅 𝐵 )
3 2 adantrl ⊢ ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ¬ 𝐵 𝑅 𝐵 )
4 3 pm2.21d ⊢ ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐵 𝑅 𝐵 → 𝐴 ≠ 𝐵 ) )
5 4 ex ⊢ ( 𝑅 Po 𝑉 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 𝑅 𝐵 → 𝐴 ≠ 𝐵 ) ) )
6 5 com13 ⊢ ( 𝐵 𝑅 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑅 Po 𝑉 → 𝐴 ≠ 𝐵 ) ) )
7 1 6 biimtrdi ⊢ ( 𝐴 = 𝐵 → ( 𝐴 𝑅 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑅 Po 𝑉 → 𝐴 ≠ 𝐵 ) ) ) )
8 7 com24 ⊢ ( 𝐴 = 𝐵 → ( 𝑅 Po 𝑉 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝑅 𝐵 → 𝐴 ≠ 𝐵 ) ) ) )
9 8 3impd ⊢ ( 𝐴 = 𝐵 → ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 ) )
10 ax-1 ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 ) )
11 9 10 pm2.61ine ⊢ ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 )