f1resrcmplf1dlem

	Ref	Expression
Hypotheses	f1resrcmplf1dlem.1	$⊢ φ \to C \subseteq A$
	f1resrcmplf1dlem.2	$⊢ φ \to D \subseteq A$
	f1resrcmplf1dlem.3	$⊢ φ \to F : A ⟶ B$
	f1resrcmplf1dlem.4	$⊢ φ \to F [C] \cap F [D] = \emptyset$
Assertion	f1resrcmplf1dlem	$⊢ φ \to ((X \in C \land Y \in D) \to (F (X) = F (Y) \to X = Y))$

Step	Hyp	Ref	Expression
1		f1resrcmplf1dlem.1	$⊢ φ \to C \subseteq A$
2		f1resrcmplf1dlem.2	$⊢ φ \to D \subseteq A$
3		f1resrcmplf1dlem.3	$⊢ φ \to F : A ⟶ B$
4		f1resrcmplf1dlem.4	$⊢ φ \to F [C] \cap F [D] = \emptyset$
5	3	ffnd	$⊢ φ \to F Fn A$
6		fnfvima	$⊢ (F Fn A \land C \subseteq A \land X \in C) \to F (X) \in F [C]$
7	5 6	syl3an1	$⊢ (φ \land C \subseteq A \land X \in C) \to F (X) \in F [C]$
8	1 7	syl3an2	$⊢ (φ \land φ \land X \in C) \to F (X) \in F [C]$
9	8	3anidm12	$⊢ (φ \land X \in C) \to F (X) \in F [C]$
10	9	ex	$⊢ φ \to (X \in C \to F (X) \in F [C])$
11		fnfvima	$⊢ (F Fn A \land D \subseteq A \land Y \in D) \to F (Y) \in F [D]$
12	5 11	syl3an1	$⊢ (φ \land D \subseteq A \land Y \in D) \to F (Y) \in F [D]$
13	2 12	syl3an2	$⊢ (φ \land φ \land Y \in D) \to F (Y) \in F [D]$
14	13	3anidm12	$⊢ (φ \land Y \in D) \to F (Y) \in F [D]$
15	14	ex	$⊢ φ \to (Y \in D \to F (Y) \in F [D])$
16		disjne	$⊢ (F [C] \cap F [D] = \emptyset \land F (X) \in F [C] \land F (Y) \in F [D]) \to F (X) \neq F (Y)$
17	4 16	syl3an1	$⊢ (φ \land F (X) \in F [C] \land F (Y) \in F [D]) \to F (X) \neq F (Y)$
18	17	3expib	$⊢ φ \to ((F (X) \in F [C] \land F (Y) \in F [D]) \to F (X) \neq F (Y))$
19		neneq	$⊢ F (X) \neq F (Y) \to \neg F (X) = F (Y)$
20	19	pm2.21d	$⊢ F (X) \neq F (Y) \to (F (X) = F (Y) \to X = Y)$
21	18 20	syl6	$⊢ φ \to ((F (X) \in F [C] \land F (Y) \in F [D]) \to (F (X) = F (Y) \to X = Y))$
22	10 15 21	syl2and	$⊢ φ \to ((X \in C \land Y \in D) \to (F (X) = F (Y) \to X = Y))$

Metamath Proof Explorer