Theorem predprc

Description: The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024)

	Ref	Expression
Assertion	predprc	⊢ ( ¬ 𝑋 ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
2		snprc	⊢ ( ¬ 𝑋 ∈ V ↔ { 𝑋 } = ∅ )
3	2	biimpi	⊢ ( ¬ 𝑋 ∈ V → { 𝑋 } = ∅ )
4	3	imaeq2d	⊢ ( ¬ 𝑋 ∈ V → ( ◡ 𝑅 “ { 𝑋 } ) = ( ◡ 𝑅 “ ∅ ) )
5		ima0	⊢ ( ◡ 𝑅 “ ∅ ) = ∅
6	4 5	eqtrdi	⊢ ( ¬ 𝑋 ∈ V → ( ◡ 𝑅 “ { 𝑋 } ) = ∅ )
7	6	ineq2d	⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ∅ ) )
8		in0	⊢ ( 𝐴 ∩ ∅ ) = ∅
9	7 8	eqtrdi	⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ∅ )
10	1 9	eqtrid	⊢ ( ¬ 𝑋 ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) = ∅ )