Theorem f1imapss

Description: Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014)

	Ref	Expression
Assertion	f1imapss	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\subseteq A\wedge D\subseteq A\right)\right)\to \left(F\left[C\right]\subset F\left[D\right]\leftrightarrow C\subset D\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1imass	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\subseteq A\wedge D\subseteq A\right)\right)\to \left(F\left[C\right]\subseteq F\left[D\right]\leftrightarrow C\subseteq D\right)$$
2		f1imaeq	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\subseteq A\wedge D\subseteq A\right)\right)\to \left(F\left[C\right]=F\left[D\right]\leftrightarrow C=D\right)$$
3	2	notbid	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\subseteq A\wedge D\subseteq A\right)\right)\to \left(\neg F\left[C\right]=F\left[D\right]\leftrightarrow \neg C=D\right)$$
4	1 3	anbi12d	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\subseteq A\wedge D\subseteq A\right)\right)\to \left(\left(F\left[C\right]\subseteq F\left[D\right]\wedge \neg F\left[C\right]=F\left[D\right]\right)\leftrightarrow \left(C\subseteq D\wedge \neg C=D\right)\right)$$
5		dfpss2	$$⊢F\left[C\right]\subset F\left[D\right]\leftrightarrow \left(F\left[C\right]\subseteq F\left[D\right]\wedge \neg F\left[C\right]=F\left[D\right]\right)$$
6		dfpss2	$$⊢C\subset D\leftrightarrow \left(C\subseteq D\wedge \neg C=D\right)$$
7	4 5 6	3bitr4g	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\subseteq A\wedge D\subseteq A\right)\right)\to \left(F\left[C\right]\subset F\left[D\right]\leftrightarrow C\subset D\right)$$