Theorem f1resrcmplf1dlem

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

	Ref	Expression
Hypotheses	f1resrcmplf1dlem.1	|- ( ph -> C C_ A )
	f1resrcmplf1dlem.2	|- ( ph -> D C_ A )
	f1resrcmplf1dlem.3	|- ( ph -> F : A --> B )
	f1resrcmplf1dlem.4	|- ( ph -> ( ( F " C ) i^i ( F " D ) ) = (/) )
	f1resrcmplf1dlem.x	|- ( ph -> X e. C )
	f1resrcmplf1dlem.y	|- ( ph -> Y e. D )
	f1resrcmplf1dlem.5	|- ( ph -> ( F ` X ) = ( F ` Y ) )
Assertion	f1resrcmplf1dlem	|- ( ph -> X = Y )

Proof

Step	Hyp	Ref	Expression
1		f1resrcmplf1dlem.1	|- ( ph -> C C_ A )
2		f1resrcmplf1dlem.2	|- ( ph -> D C_ A )
3		f1resrcmplf1dlem.3	|- ( ph -> F : A --> B )
4		f1resrcmplf1dlem.4	|- ( ph -> ( ( F " C ) i^i ( F " D ) ) = (/) )
5		f1resrcmplf1dlem.x	|- ( ph -> X e. C )
6		f1resrcmplf1dlem.y	|- ( ph -> Y e. D )
7		f1resrcmplf1dlem.5	|- ( ph -> ( F ` X ) = ( F ` Y ) )
8	5 6	jca	|- ( ph -> ( X e. C /\ Y e. D ) )
9	3	ffnd	|- ( ph -> F Fn A )
10		fnfvima	|- ( ( F Fn A /\ C C_ A /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
11	9 10	syl3an1	|- ( ( ph /\ C C_ A /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
12	1 11	syl3an2	|- ( ( ph /\ ph /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
13	12	3anidm12	|- ( ( ph /\ X e. C ) -> ( F ` X ) e. ( F " C ) )
14	13	ex	|- ( ph -> ( X e. C -> ( F ` X ) e. ( F " C ) ) )
15		fnfvima	|- ( ( F Fn A /\ D C_ A /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
16	9 15	syl3an1	|- ( ( ph /\ D C_ A /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
17	2 16	syl3an2	|- ( ( ph /\ ph /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
18	17	3anidm12	|- ( ( ph /\ Y e. D ) -> ( F ` Y ) e. ( F " D ) )
19	18	ex	|- ( ph -> ( Y e. D -> ( F ` Y ) e. ( F " D ) ) )
20		disjne	|- ( ( ( ( F " C ) i^i ( F " D ) ) = (/) /\ ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( F ` X ) =/= ( F ` Y ) )
21	4 20	syl3an1	|- ( ( ph /\ ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( F ` X ) =/= ( F ` Y ) )
22	21	3expib	|- ( ph -> ( ( ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( F ` X ) =/= ( F ` Y ) ) )
23		neneq	|- ( ( F ` X ) =/= ( F ` Y ) -> -. ( F ` X ) = ( F ` Y ) )
24	23	pm2.21d	|- ( ( F ` X ) =/= ( F ` Y ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
25	22 24	syl6	|- ( ph -> ( ( ( F ` X ) e. ( F " C ) /\ ( F ` Y ) e. ( F " D ) ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
26	14 19 25	syl2and	|- ( ph -> ( ( X e. C /\ Y e. D ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
27	8 26	mpd	|- ( ph -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
28	7 27	mpd	|- ( ph -> X = Y )