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	syl6bi	⊢ ( 𝐴 = 𝐵 → ( 𝐴 𝑅 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑅 Po 𝑉 → 𝐴 ≠ 𝐵 ) ) ) )
8	7	com24	⊢ ( 𝐴 = 𝐵 → ( 𝑅 Po 𝑉 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝑅 𝐵 → 𝐴 ≠ 𝐵 ) ) ) )
9	8	3impd	⊢ ( 𝐴 = 𝐵 → ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 ) )
10		ax-1	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 ) )
11	9 10	pm2.61ine	⊢ ( ( 𝑅 Po 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ≠ 𝐵 )