Theorem predres

Description: Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024)

	Ref	Expression
Assertion	predres	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } ⊆ 𝐴
2		sseqin2	⊢ ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } ⊆ 𝐴 ↔ ( 𝐴 ∩ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )
3	1 2	mpbi	⊢ ( 𝐴 ∩ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 }
4		dfrab2	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } = ( { 𝑦 ∣ 𝑦 𝑅 𝑋 } ∩ 𝐴 )
5	3 4	eqtr2i	⊢ ( { 𝑦 ∣ 𝑦 𝑅 𝑋 } ∩ 𝐴 ) = ( 𝐴 ∩ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )
6		iniseg	⊢ ( 𝑋 ∈ V → ( ◡ 𝑅 “ { 𝑋 } ) = { 𝑦 ∣ 𝑦 𝑅 𝑋 } )
7	6	ineq2d	⊢ ( 𝑋 ∈ V → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } ) )
8		incom	⊢ ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } ) = ( { 𝑦 ∣ 𝑦 𝑅 𝑋 } ∩ 𝐴 )
9	7 8	eqtrdi	⊢ ( 𝑋 ∈ V → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( { 𝑦 ∣ 𝑦 𝑅 𝑋 } ∩ 𝐴 ) )
10		iniseg	⊢ ( 𝑋 ∈ V → ( ◡ ( 𝑅 ↾ 𝐴 ) “ { 𝑋 } ) = { 𝑦 ∣ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑋 } )
11		brres	⊢ ( 𝑋 ∈ V → ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑋 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑋 ) ) )
12	11	abbidv	⊢ ( 𝑋 ∈ V → { 𝑦 ∣ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑋 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑋 ) } )
13		df-rab	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑋 ) }
14	12 13	eqtr4di	⊢ ( 𝑋 ∈ V → { 𝑦 ∣ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑋 } = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )
15	10 14	eqtrd	⊢ ( 𝑋 ∈ V → ( ◡ ( 𝑅 ↾ 𝐴 ) “ { 𝑋 } ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )
16	15	ineq2d	⊢ ( 𝑋 ∈ V → ( 𝐴 ∩ ( ◡ ( 𝑅 ↾ 𝐴 ) “ { 𝑋 } ) ) = ( 𝐴 ∩ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } ) )
17	5 9 16	3eqtr4a	⊢ ( 𝑋 ∈ V → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ ( 𝑅 ↾ 𝐴 ) “ { 𝑋 } ) ) )
18		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
19		df-pred	⊢ Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ ( 𝑅 ↾ 𝐴 ) “ { 𝑋 } ) )
20	17 18 19	3eqtr4g	⊢ ( 𝑋 ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 ) )
21		predprc	⊢ ( ¬ 𝑋 ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) = ∅ )
22		predprc	⊢ ( ¬ 𝑋 ∈ V → Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 ) = ∅ )
23	21 22	eqtr4d	⊢ ( ¬ 𝑋 ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 ) )
24	20 23	pm2.61i	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 )