Metamath Proof Explorer

Theorem resinsnALT

Description: Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion resinsnALT 
|- ( ( F |` ( A i^i { B } ) ) = (/) <-> -. B e. ( dom F i^i A ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( F |` ( A i^i { B } ) )
2 reldm0 
 |-  ( Rel ( F |` ( A i^i { B } ) ) -> ( ( F |` ( A i^i { B } ) ) = (/) <-> dom ( F |` ( A i^i { B } ) ) = (/) ) )
3 1 2 ax-mp 
 |-  ( ( F |` ( A i^i { B } ) ) = (/) <-> dom ( F |` ( A i^i { B } ) ) = (/) )
4 dmres 
 |-  dom ( F |` ( A i^i { B } ) ) = ( ( A i^i { B } ) i^i dom F )
5 incom 
 |-  ( ( A i^i { B } ) i^i dom F ) = ( dom F i^i ( A i^i { B } ) )
6 4 5 eqtri 
 |-  dom ( F |` ( A i^i { B } ) ) = ( dom F i^i ( A i^i { B } ) )
7 6 eqeq1i 
 |-  ( dom ( F |` ( A i^i { B } ) ) = (/) <-> ( dom F i^i ( A i^i { B } ) ) = (/) )
8 elin 
 |-  ( B e. ( dom F i^i A ) <-> ( B e. dom F /\ B e. A ) )
9 ancom 
 |-  ( ( B e. dom F /\ B e. A ) <-> ( B e. A /\ B e. dom F ) )
10 snssi 
 |-  ( B e. A -> { B } C_ A )
11 incom 
 |-  ( A i^i { B } ) = ( { B } i^i A )
12 dfss2 
 |-  ( { B } C_ A <-> ( { B } i^i A ) = { B } )
13 12 biimpi 
 |-  ( { B } C_ A -> ( { B } i^i A ) = { B } )
14 11 13 eqtrid 
 |-  ( { B } C_ A -> ( A i^i { B } ) = { B } )
15 10 14 syl 
 |-  ( B e. A -> ( A i^i { B } ) = { B } )
16 15 ineq2d 
 |-  ( B e. A -> ( dom F i^i ( A i^i { B } ) ) = ( dom F i^i { B } ) )
17 16 eqeq1d 
 |-  ( B e. A -> ( ( dom F i^i ( A i^i { B } ) ) = (/) <-> ( dom F i^i { B } ) = (/) ) )
18 disjsn 
 |-  ( ( dom F i^i { B } ) = (/) <-> -. B e. dom F )
19 17 18 bitrdi 
 |-  ( B e. A -> ( ( dom F i^i ( A i^i { B } ) ) = (/) <-> -. B e. dom F ) )
20 disjsn 
 |-  ( ( A i^i { B } ) = (/) <-> -. B e. A )
21 20 biimpri 
 |-  ( -. B e. A -> ( A i^i { B } ) = (/) )
22 21 ineq2d 
 |-  ( -. B e. A -> ( dom F i^i ( A i^i { B } ) ) = ( dom F i^i (/) ) )
23 in0 
 |-  ( dom F i^i (/) ) = (/)
24 22 23 eqtrdi 
 |-  ( -. B e. A -> ( dom F i^i ( A i^i { B } ) ) = (/) )
25 19 24 resinsnlem 
 |-  ( ( B e. A /\ B e. dom F ) <-> -. ( dom F i^i ( A i^i { B } ) ) = (/) )
26 8 9 25 3bitri 
 |-  ( B e. ( dom F i^i A ) <-> -. ( dom F i^i ( A i^i { B } ) ) = (/) )
27 26 con2bii 
 |-  ( ( dom F i^i ( A i^i { B } ) ) = (/) <-> -. B e. ( dom F i^i A ) )
28 3 7 27 3bitri 
 |-  ( ( F |` ( A i^i { B } ) ) = (/) <-> -. B e. ( dom F i^i A ) )