Theorem elsetpreimafveq

Description: If two preimages of function values contain elements with identical function values, then both preimages are equal. (Contributed by AV, 8-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
Assertion	elsetpreimafveq	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑆 = 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		eqeq2	⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) ) )
3	2	rabbidv	⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) } )
4	3	adantl	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) } )
5		id	⊢ ( 𝐹 Fn 𝐴 → 𝐹 Fn 𝐴 )
6		simpl	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) → 𝑆 ∈ 𝑃 )
7		simpl	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) → 𝑋 ∈ 𝑆 )
8	5 6 7	3anim123i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) )
9	8	adantr	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) )
10	1	elsetpreimafvrab	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } )
11	9 10	syl	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑆 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) } )
12		simpr	⊢ ( ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) → 𝑅 ∈ 𝑃 )
13		simpr	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) → 𝑌 ∈ 𝑅 )
14	5 12 13	3anim123i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 Fn 𝐴 ∧ 𝑅 ∈ 𝑃 ∧ 𝑌 ∈ 𝑅 ) )
15	14	adantr	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → ( 𝐹 Fn 𝐴 ∧ 𝑅 ∈ 𝑃 ∧ 𝑌 ∈ 𝑅 ) )
16	1	elsetpreimafvrab	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑅 ∈ 𝑃 ∧ 𝑌 ∈ 𝑅 ) → 𝑅 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) } )
17	15 16	syl	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑅 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑌 ) } )
18	4 11 17	3eqtr4d	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) → 𝑆 = 𝑅 )
19	18	ex	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑆 = 𝑅 ) )