Theorem f1resrcmplf1dlem

Description: Lemma for f1resrcmplf1d . (Contributed by BTernaryTau, 27-Sep-2023) (Revised by Mingli Yuan, 15-Aug-2026)

	Ref	Expression
Hypotheses	f1resrcmplf1dlem.1	$$⊢\phi \to C\subseteq A$$
	f1resrcmplf1dlem.2	$$⊢\phi \to D\subseteq A$$
	f1resrcmplf1dlem.3	$$⊢\phi \to F:A⟶B$$
	f1resrcmplf1dlem.4	$$⊢\phi \to F\left[C\right]\cap F\left[D\right]=\varnothing$$
	f1resrcmplf1dlem.x	$$⊢\phi \to X\in C$$
	f1resrcmplf1dlem.y	$$⊢\phi \to Y\in D$$
	f1resrcmplf1dlem.5	$$⊢\phi \to F\left(X\right)=F\left(Y\right)$$
Assertion	f1resrcmplf1dlem	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		f1resrcmplf1dlem.1	$$⊢\phi \to C\subseteq A$$
2		f1resrcmplf1dlem.2	$$⊢\phi \to D\subseteq A$$
3		f1resrcmplf1dlem.3	$$⊢\phi \to F:A⟶B$$
4		f1resrcmplf1dlem.4	$$⊢\phi \to F\left[C\right]\cap F\left[D\right]=\varnothing$$
5		f1resrcmplf1dlem.x	$$⊢\phi \to X\in C$$
6		f1resrcmplf1dlem.y	$$⊢\phi \to Y\in D$$
7		f1resrcmplf1dlem.5	$$⊢\phi \to F\left(X\right)=F\left(Y\right)$$
8	5 6	jca	$$⊢\phi \to \left(X\in C\wedge Y\in D\right)$$
9	3	ffnd	$$⊢\phi \to FFnA$$
10		fnfvima	$$⊢\left(FFnA\wedge C\subseteq A\wedge X\in C\right)\to F\left(X\right)\in F\left[C\right]$$
11	9 10	syl3an1	$$⊢\left(\phi \wedge C\subseteq A\wedge X\in C\right)\to F\left(X\right)\in F\left[C\right]$$
12	1 11	syl3an2	$$⊢\left(\phi \wedge \phi \wedge X\in C\right)\to F\left(X\right)\in F\left[C\right]$$
13	12	3anidm12	$$⊢\left(\phi \wedge X\in C\right)\to F\left(X\right)\in F\left[C\right]$$
14	13	ex	$$⊢\phi \to \left(X\in C\to F\left(X\right)\in F\left[C\right]\right)$$
15		fnfvima	$$⊢\left(FFnA\wedge D\subseteq A\wedge Y\in D\right)\to F\left(Y\right)\in F\left[D\right]$$
16	9 15	syl3an1	$$⊢\left(\phi \wedge D\subseteq A\wedge Y\in D\right)\to F\left(Y\right)\in F\left[D\right]$$
17	2 16	syl3an2	$$⊢\left(\phi \wedge \phi \wedge Y\in D\right)\to F\left(Y\right)\in F\left[D\right]$$
18	17	3anidm12	$$⊢\left(\phi \wedge Y\in D\right)\to F\left(Y\right)\in F\left[D\right]$$
19	18	ex	$$⊢\phi \to \left(Y\in D\to F\left(Y\right)\in F\left[D\right]\right)$$
20		disjne	$$⊢\left(F\left[C\right]\cap F\left[D\right]=\varnothing \wedge F\left(X\right)\in F\left[C\right]\wedge F\left(Y\right)\in F\left[D\right]\right)\to F\left(X\right)\ne F\left(Y\right)$$
21	4 20	syl3an1	$$⊢\left(\phi \wedge F\left(X\right)\in F\left[C\right]\wedge F\left(Y\right)\in F\left[D\right]\right)\to F\left(X\right)\ne F\left(Y\right)$$
22	21	3expib	$$⊢\phi \to \left(\left(F\left(X\right)\in F\left[C\right]\wedge F\left(Y\right)\in F\left[D\right]\right)\to F\left(X\right)\ne F\left(Y\right)\right)$$
23		neneq	$$⊢F\left(X\right)\ne F\left(Y\right)\to \neg F\left(X\right)=F\left(Y\right)$$
24	23	pm2.21d	$$⊢F\left(X\right)\ne F\left(Y\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
25	22 24	syl6	$$⊢\phi \to \left(\left(F\left(X\right)\in F\left[C\right]\wedge F\left(Y\right)\in F\left[D\right]\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
26	14 19 25	syl2and	$$⊢\phi \to \left(\left(X\in C\wedge Y\in D\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
27	8 26	mpd	$$⊢\phi \to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
28	7 27	mpd	$$⊢\phi \to X=Y$$