f1imass

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

		Ref	Expression
	Assertion	f1imass	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [C] \subseteq F [D] \leftrightarrow C \subseteq D)$

Proof

Step	Hyp	Ref	Expression
1		simplrl	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \to C \subseteq A$
2	1	sseld	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \to (a \in C \to a \in A)$
3		simplr	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to F [C] \subseteq F [D]$
4	3	sseld	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to (F (a) \in F [C] \to F (a) \in F [D])$
5		simplll	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to F : A \underset{1-1}{⟶} B$
6		simpr	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to a \in A$
7		simp1rl	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D] \land a \in A) \to C \subseteq A$
8	7	3expa	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to C \subseteq A$
9		f1elima	$⊢ (F : A \underset{1-1}{⟶} B \land a \in A \land C \subseteq A) \to (F (a) \in F [C] \leftrightarrow a \in C)$
10	5 6 8 9	syl3anc	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to (F (a) \in F [C] \leftrightarrow a \in C)$
11		simp1rr	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D] \land a \in A) \to D \subseteq A$
12	11	3expa	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to D \subseteq A$
13		f1elima	$⊢ (F : A \underset{1-1}{⟶} B \land a \in A \land D \subseteq A) \to (F (a) \in F [D] \leftrightarrow a \in D)$
14	5 6 12 13	syl3anc	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to (F (a) \in F [D] \leftrightarrow a \in D)$
15	4 10 14	3imtr3d	$⊢ (((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \land a \in A) \to (a \in C \to a \in D)$
16	15	ex	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \to (a \in A \to (a \in C \to a \in D))$
17	2 16	syld	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \to (a \in C \to (a \in C \to a \in D))$
18	17	pm2.43d	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \to (a \in C \to a \in D)$
19	18	ssrdv	$⊢ ((F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \land F [C] \subseteq F [D]) \to C \subseteq D$
20	19	ex	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [C] \subseteq F [D] \to C \subseteq D)$
21		imass2	$⊢ C \subseteq D \to F [C] \subseteq F [D]$
22	20 21	impbid1	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [C] \subseteq F [D] \leftrightarrow C \subseteq D)$

Metamath Proof Explorer

Theorem f1imass

Proof