Theorem fnssintima

Description: Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024)

	Ref	Expression
Assertion	fnssintima	|- ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <-> A. x e. B C C_ ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssint	|- ( C C_ |^| ( F " B ) <-> A. y e. ( F " B ) C C_ y )
2		df-ral	|- ( A. y e. ( F " B ) C C_ y <-> A. y ( y e. ( F " B ) -> C C_ y ) )
3	1 2	bitri	|- ( C C_ |^| ( F " B ) <-> A. y ( y e. ( F " B ) -> C C_ y ) )
4		fvelimab	|- ( ( F Fn A /\ B C_ A ) -> ( y e. ( F " B ) <-> E. x e. B ( F ` x ) = y ) )
5	4	imbi1d	|- ( ( F Fn A /\ B C_ A ) -> ( ( y e. ( F " B ) -> C C_ y ) <-> ( E. x e. B ( F ` x ) = y -> C C_ y ) ) )
6	5	albidv	|- ( ( F Fn A /\ B C_ A ) -> ( A. y ( y e. ( F " B ) -> C C_ y ) <-> A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) ) )
7		ralcom4	|- ( A. x e. B A. y ( ( F ` x ) = y -> C C_ y ) <-> A. y A. x e. B ( ( F ` x ) = y -> C C_ y ) )
8		eqcom	|- ( ( F ` x ) = y <-> y = ( F ` x ) )
9	8	imbi1i	|- ( ( ( F ` x ) = y -> C C_ y ) <-> ( y = ( F ` x ) -> C C_ y ) )
10	9	albii	|- ( A. y ( ( F ` x ) = y -> C C_ y ) <-> A. y ( y = ( F ` x ) -> C C_ y ) )
11		fvex	|- ( F ` x ) e. _V
12		sseq2	|- ( y = ( F ` x ) -> ( C C_ y <-> C C_ ( F ` x ) ) )
13	11 12	ceqsalv	|- ( A. y ( y = ( F ` x ) -> C C_ y ) <-> C C_ ( F ` x ) )
14	10 13	bitri	|- ( A. y ( ( F ` x ) = y -> C C_ y ) <-> C C_ ( F ` x ) )
15	14	ralbii	|- ( A. x e. B A. y ( ( F ` x ) = y -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) )
16		r19.23v	|- ( A. x e. B ( ( F ` x ) = y -> C C_ y ) <-> ( E. x e. B ( F ` x ) = y -> C C_ y ) )
17	16	albii	|- ( A. y A. x e. B ( ( F ` x ) = y -> C C_ y ) <-> A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) )
18	7 15 17	3bitr3ri	|- ( A. y ( E. x e. B ( F ` x ) = y -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) )
19	6 18	bitrdi	|- ( ( F Fn A /\ B C_ A ) -> ( A. y ( y e. ( F " B ) -> C C_ y ) <-> A. x e. B C C_ ( F ` x ) ) )
20	3 19	bitrid	|- ( ( F Fn A /\ B C_ A ) -> ( C C_ |^| ( F " B ) <-> A. x e. B C C_ ( F ` x ) ) )