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

Metamath Proof Explorer

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 ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑋 )