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 𝐴𝑅𝐹 ) ) )