Theorem ssimaexg

Description: The existence of a subimage. (Contributed by FL, 15-Apr-2007)

	Ref	Expression
Assertion	ssimaexg	$$⊢\left(A\in C\wedge \mathrm{Fun}F\wedge B\subseteq F\left[A\right]\right)\to \exists x\left(x\subseteq A\wedge B=F\left[x\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		imaeq2	$$⊢y=A\to F\left[y\right]=F\left[A\right]$$
2	1	sseq2d	$$⊢y=A\to \left(B\subseteq F\left[y\right]\leftrightarrow B\subseteq F\left[A\right]\right)$$
3	2	anbi2d	$$⊢y=A\to \left(\left(\mathrm{Fun}F\wedge B\subseteq F\left[y\right]\right)\leftrightarrow \left(\mathrm{Fun}F\wedge B\subseteq F\left[A\right]\right)\right)$$
4		sseq2	$$⊢y=A\to \left(x\subseteq y\leftrightarrow x\subseteq A\right)$$
5	4	anbi1d	$$⊢y=A\to \left(\left(x\subseteq y\wedge B=F\left[x\right]\right)\leftrightarrow \left(x\subseteq A\wedge B=F\left[x\right]\right)\right)$$
6	5	exbidv	$$⊢y=A\to \left(\exists x\left(x\subseteq y\wedge B=F\left[x\right]\right)\leftrightarrow \exists x\left(x\subseteq A\wedge B=F\left[x\right]\right)\right)$$
7	3 6	imbi12d	$$⊢y=A\to \left(\left(\left(\mathrm{Fun}F\wedge B\subseteq F\left[y\right]\right)\to \exists x\left(x\subseteq y\wedge B=F\left[x\right]\right)\right)\leftrightarrow \left(\left(\mathrm{Fun}F\wedge B\subseteq F\left[A\right]\right)\to \exists x\left(x\subseteq A\wedge B=F\left[x\right]\right)\right)\right)$$
8		vex	$$⊢y\in \mathrm{V}$$
9	8	ssimaex	$$⊢\left(\mathrm{Fun}F\wedge B\subseteq F\left[y\right]\right)\to \exists x\left(x\subseteq y\wedge B=F\left[x\right]\right)$$
10	7 9	vtoclg	$$⊢A\in C\to \left(\left(\mathrm{Fun}F\wedge B\subseteq F\left[A\right]\right)\to \exists x\left(x\subseteq A\wedge B=F\left[x\right]\right)\right)$$
11	10	3impib	$$⊢\left(A\in C\wedge \mathrm{Fun}F\wedge B\subseteq F\left[A\right]\right)\to \exists x\left(x\subseteq A\wedge B=F\left[x\right]\right)$$