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

Metamath Proof Explorer

Theorem fnresdisj

Description: A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion fnresdisj ( 𝐹 Fn 𝐴 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐹 ↾ 𝐵 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( 𝐹 ↾ 𝐵 )
2 reldm0 ⊢ ( Rel ( 𝐹 ↾ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) = ∅ ↔ dom ( 𝐹 ↾ 𝐵 ) = ∅ ) )
3 1 2 ax-mp ⊢ ( ( 𝐹 ↾ 𝐵 ) = ∅ ↔ dom ( 𝐹 ↾ 𝐵 ) = ∅ )
4 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
5 incom ⊢ ( 𝐵 ∩ dom 𝐹 ) = ( dom 𝐹 ∩ 𝐵 )
6 4 5 eqtri ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( dom 𝐹 ∩ 𝐵 )
7 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
8 7 ineq1d ⊢ ( 𝐹 Fn 𝐴 → ( dom 𝐹 ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
9 6 8 eqtrid ⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ↾ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
10 9 eqeq1d ⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
11 3 10 bitr2id ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐹 ↾ 𝐵 ) = ∅ ) )