Metamath Proof Explorer


Theorem elpredimg

Description: Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 13-Apr-2011) (Revised by NM, 5-Apr-2016) (Proof shortened by BJ, 16-Oct-2024)

Ref Expression
Assertion elpredimg ( ( 𝑋𝑉𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 𝑅 𝑋 )

Proof

Step Hyp Ref Expression
1 elpredgg ( ( 𝑋𝑉𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌𝐴𝑌 𝑅 𝑋 ) ) )
2 simpr ( ( 𝑌𝐴𝑌 𝑅 𝑋 ) → 𝑌 𝑅 𝑋 )
3 1 2 biimtrdi ( ( 𝑋𝑉𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 𝑅 𝑋 ) )
4 3 syldbl2 ( ( 𝑋𝑉𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 𝑅 𝑋 )