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

Metamath Proof Explorer

Theorem predidm

Description: Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011)

Ref Expression
Assertion predidm Pred ( 𝑅 , Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 )

Proof

Step Hyp Ref Expression
1 df-pred ⊢ Pred ( 𝑅 , Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝑋 ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
2 df-pred ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3 inidm ⊢ ( ( ◡ 𝑅 “ { 𝑋 } ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ◡ 𝑅 “ { 𝑋 } )
4 3 ineq2i ⊢ ( 𝐴 ∩ ( ( ◡ 𝑅 “ { 𝑋 } ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
5 2 4 eqtr4i ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ( ◡ 𝑅 “ { 𝑋 } ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
6 inass ⊢ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ( ◡ 𝑅 “ { 𝑋 } ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
7 5 6 eqtr4i ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
8 2 ineq1i ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
9 7 8 eqtr4i ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
10 1 9 eqtr4i ⊢ Pred ( 𝑅 , Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 )