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

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 dfss2 ⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
4 2 3 sylib ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
5 4 imaeq2d ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) = ( 𝑅 “ { 𝐵 } ) )
6 5 ineq1d ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 ) = ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) )
7 imass2 ⊢ ( { 𝐵 } ⊆ 𝐴 → ( 𝑅 “ { 𝐵 } ) ⊆ ( 𝑅 “ 𝐴 ) )
8 2 7 syl ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ { 𝐵 } ) ⊆ ( 𝑅 “ 𝐴 ) )
9 simpl ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
10 8 9 sstrd ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ { 𝐵 } ) ⊆ 𝐴 )
11 dfss2 ⊢ ( ( 𝑅 “ { 𝐵 } ) ⊆ 𝐴 ↔ ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) = ( 𝑅 “ { 𝐵 } ) )
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 ⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 = [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )