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

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 imbitrrid ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑅 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 ( 𝑅 , 𝐴 , 𝑋 ) )