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