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

Metamath Proof Explorer

Theorem eqresfnbd

Description: Property of being the restriction of a function. Note that this is closer to funssres than fnssres . (Contributed by SN, 11-Mar-2025)

Ref Expression
Hypotheses eqresfnbd.g ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
eqresfnbd.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion eqresfnbd ( 𝜑 → ( 𝑅 = ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 eqresfnbd.g ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
2 eqresfnbd.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3 1 2 fnssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
4 resss ⊢ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹
5 3 4 jctir ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 ) )
6 fneq1 ⊢ ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅 Fn 𝐴 ↔ ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ) )
7 sseq1 ⊢ ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅 ⊆ 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 ) )
8 6 7 anbi12d ⊢ ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ↔ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 ) ) )
9 5 8 syl5ibrcom ⊢ ( 𝜑 → ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ) )
10 1 fnfund ⊢ ( 𝜑 → Fun 𝐹 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → Fun 𝐹 )
12 funssres ⊢ ( ( Fun 𝐹 ∧ 𝑅 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝑅 ) = 𝑅 )
13 12 eqcomd ⊢ ( ( Fun 𝐹 ∧ 𝑅 ⊆ 𝐹 ) → 𝑅 = ( 𝐹 ↾ dom 𝑅 ) )
14 fndm ⊢ ( 𝑅 Fn 𝐴 → dom 𝑅 = 𝐴 )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → dom 𝑅 = 𝐴 )
16 15 reseq2d ⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( 𝐹 ↾ dom 𝑅 ) = ( 𝐹 ↾ 𝐴 ) )
17 16 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( 𝑅 = ( 𝐹 ↾ dom 𝑅 ) ↔ 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
18 13 17 imbitrid ⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( ( Fun 𝐹 ∧ 𝑅 ⊆ 𝐹 ) → 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
19 11 18 mpand ⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( 𝑅 ⊆ 𝐹 → 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
20 19 expimpd ⊢ ( 𝜑 → ( ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) → 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
21 9 20 impbid ⊢ ( 𝜑 → ( 𝑅 = ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ) )