Theorem f1resrcmplf1dlem

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

	Ref	Expression
Hypotheses	f1resrcmplf1dlem.1	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	f1resrcmplf1dlem.2	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
	f1resrcmplf1dlem.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	f1resrcmplf1dlem.4	⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ 𝐷 ) ) = ∅ )
	f1resrcmplf1dlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
	f1resrcmplf1dlem.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
	f1resrcmplf1dlem.5	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
Assertion	f1resrcmplf1dlem	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		f1resrcmplf1dlem.1	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
2		f1resrcmplf1dlem.2	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
3		f1resrcmplf1dlem.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
4		f1resrcmplf1dlem.4	⊢ ( 𝜑 → ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ 𝐷 ) ) = ∅ )
5		f1resrcmplf1dlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
6		f1resrcmplf1dlem.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
7		f1resrcmplf1dlem.5	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
8	5 6	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷 ) )
9	3	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
10		fnfvima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
11	9 10	syl3an1	⊢ ( ( 𝜑 ∧ 𝐶 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
12	1 11	syl3an2	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
13	12	3anidm12	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) )
14	13	ex	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ) )
15		fnfvima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
16	9 15	syl3an1	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ 𝐴 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
17	2 16	syl3an2	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
18	17	3anidm12	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) )
19	18	ex	⊢ ( 𝜑 → ( 𝑌 ∈ 𝐷 → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) )
20		disjne	⊢ ( ( ( ( 𝐹 “ 𝐶 ) ∩ ( 𝐹 “ 𝐷 ) ) = ∅ ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) )
21	4 20	syl3an1	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) )
22	21	3expib	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
23		neneq	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) → ¬ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
24	23	pm2.21d	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
25	22 24	syl6	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐹 “ 𝐶 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( 𝐹 “ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
26	14 19 25	syl2and	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
27	8 26	mpd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
28	7 27	mpd	⊢ ( 𝜑 → 𝑋 = 𝑌 )