Theorem elsetpreimafvssdm

Description: An element of the class P of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	elsetpreimafvssdm	|- ( ( F Fn A /\ S e. P ) -> S C_ A )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2	1	elsetpreimafv	|- ( S e. P -> E. x e. A S = ( `' F " { ( F ` x ) } ) )
3		cnvimass	|- ( `' F " { ( F ` x ) } ) C_ dom F
4		fndm	|- ( F Fn A -> dom F = A )
5	3 4	sseqtrid	|- ( F Fn A -> ( `' F " { ( F ` x ) } ) C_ A )
6	5	adantr	|- ( ( F Fn A /\ x e. A ) -> ( `' F " { ( F ` x ) } ) C_ A )
7		sseq1	|- ( S = ( `' F " { ( F ` x ) } ) -> ( S C_ A <-> ( `' F " { ( F ` x ) } ) C_ A ) )
8	6 7	syl5ibrcom	|- ( ( F Fn A /\ x e. A ) -> ( S = ( `' F " { ( F ` x ) } ) -> S C_ A ) )
9	8	expcom	|- ( x e. A -> ( F Fn A -> ( S = ( `' F " { ( F ` x ) } ) -> S C_ A ) ) )
10	9	com23	|- ( x e. A -> ( S = ( `' F " { ( F ` x ) } ) -> ( F Fn A -> S C_ A ) ) )
11	10	rexlimiv	|- ( E. x e. A S = ( `' F " { ( F ` x ) } ) -> ( F Fn A -> S C_ A ) )
12	2 11	syl	|- ( S e. P -> ( F Fn A -> S C_ A ) )
13	12	impcom	|- ( ( F Fn A /\ S e. P ) -> S C_ A )