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

Metamath Proof Explorer

Theorem fnssresb

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007)

Ref Expression
Assertion fnssresb ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-fn ⊢ ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) )
2 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3 2 funresd ⊢ ( 𝐹 Fn 𝐴 → Fun ( 𝐹 ↾ 𝐵 ) )
4 3 biantrurd ⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ↔ ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) ) )
5 ssdmres ⊢ ( 𝐵 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 )
6 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7 6 sseq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
8 5 7 bitr3id ⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )
9 4 8 bitr3d ⊢ ( 𝐹 Fn 𝐴 → ( ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) ↔ 𝐵 ⊆ 𝐴 ) )
10 1 9 bitrid ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )