Metamath Proof Explorer


Theorem predpoirr

Description: Given a partial ordering, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011)

Ref Expression
Assertion predpoirr ( 𝑅 Po 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )

Proof

Step Hyp Ref Expression
1 poirr ( ( 𝑅 Po 𝐴𝑋𝐴 ) → ¬ 𝑋 𝑅 𝑋 )
2 elpredg ( ( 𝑋𝐴𝑋𝐴 ) → ( 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑋 𝑅 𝑋 ) )
3 2 anidms ( 𝑋𝐴 → ( 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑋 𝑅 𝑋 ) )
4 3 notbid ( 𝑋𝐴 → ( ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ¬ 𝑋 𝑅 𝑋 ) )
5 1 4 syl5ibr ( 𝑋𝐴 → ( ( 𝑅 Po 𝐴𝑋𝐴 ) → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
6 5 expd ( 𝑋𝐴 → ( 𝑅 Po 𝐴 → ( 𝑋𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
7 6 pm2.43b ( 𝑅 Po 𝐴 → ( 𝑋𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
8 predel ( 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑋𝐴 )
9 8 con3i ( ¬ 𝑋𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
10 7 9 pm2.61d1 ( 𝑅 Po 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )