Theorem elpredim

Description: Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012)

	Ref	Expression
Hypothesis	elpredim.1	⊢ 𝑋 ∈ V
Assertion	elpredim	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 𝑅 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		elpredim.1	⊢ 𝑋 ∈ V
2		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3	2	elin2	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) )
4		elimasng	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ◡ 𝑅 ) )
5		opelcnvg	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ◡ 𝑅 ↔ ⟨ 𝑌 , 𝑋 ⟩ ∈ 𝑅 ) )
6	4 5	bitrd	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ ⟨ 𝑌 , 𝑋 ⟩ ∈ 𝑅 ) )
7	1 6	mpan	⊢ ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ ⟨ 𝑌 , 𝑋 ⟩ ∈ 𝑅 ) )
8	7	ibi	⊢ ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) → ⟨ 𝑌 , 𝑋 ⟩ ∈ 𝑅 )
9		df-br	⊢ ( 𝑌 𝑅 𝑋 ↔ ⟨ 𝑌 , 𝑋 ⟩ ∈ 𝑅 )
10	8 9	sylibr	⊢ ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) → 𝑌 𝑅 𝑋 )
11	3 10	simplbiim	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 𝑅 𝑋 )