Metamath Proof Explorer


Theorem ecinxp

Description: Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015)

Ref Expression
Assertion ecinxp ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → [ 𝐵 ] 𝑅 = [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → 𝐵𝐴 )
2 1 snssd ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → { 𝐵 } ⊆ 𝐴 )
3 df-ss ( { 𝐵 } ⊆ 𝐴 ↔ ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
4 2 3 sylib ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
5 4 imaeq2d ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) = ( 𝑅 “ { 𝐵 } ) )
6 5 ineq1d ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 ) = ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) )
7 imass2 ( { 𝐵 } ⊆ 𝐴 → ( 𝑅 “ { 𝐵 } ) ⊆ ( 𝑅𝐴 ) )
8 2 7 syl ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( 𝑅 “ { 𝐵 } ) ⊆ ( 𝑅𝐴 ) )
9 simpl ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( 𝑅𝐴 ) ⊆ 𝐴 )
10 8 9 sstrd ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( 𝑅 “ { 𝐵 } ) ⊆ 𝐴 )
11 df-ss ( ( 𝑅 “ { 𝐵 } ) ⊆ 𝐴 ↔ ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) = ( 𝑅 “ { 𝐵 } ) )
12 10 11 sylib ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) = ( 𝑅 “ { 𝐵 } ) )
13 6 12 eqtr2d ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( 𝑅 “ { 𝐵 } ) = ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 ) )
14 imainrect ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝐵 } ) = ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 )
15 13 14 eqtr4di ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → ( 𝑅 “ { 𝐵 } ) = ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝐵 } ) )
16 df-ec [ 𝐵 ] 𝑅 = ( 𝑅 “ { 𝐵 } )
17 df-ec [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝐵 } )
18 15 16 17 3eqtr4g ( ( ( 𝑅𝐴 ) ⊆ 𝐴𝐵𝐴 ) → [ 𝐵 ] 𝑅 = [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )