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	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ¬ 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) )

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	6	eqeq1i	⊢ ( dom ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ )
8		elin	⊢ ( 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) ↔ ( 𝐵 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝐴 ) )
9		ancom	⊢ ( ( 𝐵 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ dom 𝐹 ) )
10		snssi	⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
11		incom	⊢ ( 𝐴 ∩ { 𝐵 } ) = ( { 𝐵 } ∩ 𝐴 )
12		dfss2	⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
13	12	biimpi	⊢ ( { 𝐵 } ⊆ 𝐴 → ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
14	11 13	eqtrid	⊢ ( { 𝐵 } ⊆ 𝐴 → ( 𝐴 ∩ { 𝐵 } ) = { 𝐵 } )
15	10 14	syl	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐴 ∩ { 𝐵 } ) = { 𝐵 } )
16	15	ineq2d	⊢ ( 𝐵 ∈ 𝐴 → ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ( dom 𝐹 ∩ { 𝐵 } ) )
17	16	eqeq1d	⊢ ( 𝐵 ∈ 𝐴 → ( ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ( dom 𝐹 ∩ { 𝐵 } ) = ∅ ) )
18		disjsn	⊢ ( ( dom 𝐹 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ dom 𝐹 )
19	17 18	bitrdi	⊢ ( 𝐵 ∈ 𝐴 → ( ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ¬ 𝐵 ∈ dom 𝐹 ) )
20		disjsn	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )
21	20	biimpri	⊢ ( ¬ 𝐵 ∈ 𝐴 → ( 𝐴 ∩ { 𝐵 } ) = ∅ )
22	21	ineq2d	⊢ ( ¬ 𝐵 ∈ 𝐴 → ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ( dom 𝐹 ∩ ∅ ) )
23		in0	⊢ ( dom 𝐹 ∩ ∅ ) = ∅
24	22 23	eqtrdi	⊢ ( ¬ 𝐵 ∈ 𝐴 → ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ )
25	19 24	resinsnlem	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ dom 𝐹 ) ↔ ¬ ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ )
26	8 9 25	3bitri	⊢ ( 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) ↔ ¬ ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ )
27	26	con2bii	⊢ ( ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ¬ 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) )
28	3 7 27	3bitri	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ¬ 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) )