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

Metamath Proof Explorer

Theorem fnreseql

Description: Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion fnreseql ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑋 ) Fn 𝑋 )
2 1 3adant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑋 ) Fn 𝑋 )
3 fnssres ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐺 ↾ 𝑋 ) Fn 𝑋 )
4 3 3adant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐺 ↾ 𝑋 ) Fn 𝑋 )
5 fneqeql ⊢ ( ( ( 𝐹 ↾ 𝑋 ) Fn 𝑋 ∧ ( 𝐺 ↾ 𝑋 ) Fn 𝑋 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ) )
6 2 4 5 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ) )
7 resindir ⊢ ( ( 𝐹 ∩ 𝐺 ) ↾ 𝑋 ) = ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) )
8 7 dmeqi ⊢ dom ( ( 𝐹 ∩ 𝐺 ) ↾ 𝑋 ) = dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) )
9 dmres ⊢ dom ( ( 𝐹 ∩ 𝐺 ) ↾ 𝑋 ) = ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) )
10 8 9 eqtr3i ⊢ dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) )
11 10 eqeq1i ⊢ ( dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ↔ ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) ) = 𝑋 )
12 dfss2 ⊢ ( 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) ↔ ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) ) = 𝑋 )
13 11 12 bitr4i ⊢ ( dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ↔ 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) )
14 6 13 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )