Theorem sspred

Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011)

	Ref	Expression
Assertion	sspred	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		sseqin2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
2		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3	2	sseq1i	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ⊆ 𝐵 )
4		df-ss	⊢ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ 𝐵 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
5		in32	⊢ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
6	5	eqeq1i	⊢ ( ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ 𝐵 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
7	3 4 6	3bitri	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
8		ineq1	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
9	8	eqeq1d	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ↔ ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) )
10	9	biimpa	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) → ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
11		df-pred	⊢ Pred ( 𝑅 , 𝐵 , 𝑋 ) = ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
12	10 11 2	3eqtr4g	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
13	12	eqcomd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )
14	1 7 13	syl2anb	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )