Theorem imaelsetpreimafv

Description: The image of an element of the preimage of a function value is the singleton consisting of the function value at one of its elements. (Contributed by AV, 5-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2	1	fvelsetpreimafv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → ∃ 𝑥 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
3		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
4	3	sneqd	⊢ ( 𝑦 = 𝑥 → { ( 𝐹 ‘ 𝑦 ) } = { ( 𝐹 ‘ 𝑥 ) } )
5	4	imaeq2d	⊢ ( 𝑦 = 𝑥 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
6	5	eqeq2d	⊢ ( 𝑦 = 𝑥 → ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
7	6	cbvrexvw	⊢ ( ∃ 𝑦 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ∃ 𝑥 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
8	2 7	sylibr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → ∃ 𝑦 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
9	8	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ∃ 𝑦 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
10		imaeq2	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) → ( 𝐹 “ 𝑆 ) = ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
11	10	3ad2ant3	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) → ( 𝐹 “ 𝑆 ) = ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
12		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
13		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) = ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) )
14	12 13	syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) = ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) )
15	14	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) = ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) )
16	15	3ad2ant1	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) → ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) = ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) )
17	1	elsetpreimafvbi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
18		fnfvelrn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
19	18	snssd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝑦 ) } ⊆ ran 𝐹 )
20		dfss2	⊢ ( { ( 𝐹 ‘ 𝑦 ) } ⊆ ran 𝐹 ↔ ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑦 ) } )
21	19 20	sylib	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑦 ) } )
22	21	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑦 ) } )
23		simp3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
24	23	sneqd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → { ( 𝐹 ‘ 𝑦 ) } = { ( 𝐹 ‘ 𝑋 ) } )
25	22 24	eqtrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑋 ) } )
26	25	3expib	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑋 ) } ) )
27	26	3ad2ant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑋 ) } ) )
28	17 27	sylbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑆 → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑋 ) } ) )
29	28	imp	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑋 ) } )
30	29	3adant3	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) → ( { ( 𝐹 ‘ 𝑦 ) } ∩ ran 𝐹 ) = { ( 𝐹 ‘ 𝑋 ) } )
31	11 16 30	3eqtrd	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) → ( 𝐹 “ 𝑆 ) = { ( 𝐹 ‘ 𝑋 ) } )
32	31	rexlimdv3a	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( ∃ 𝑦 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) → ( 𝐹 “ 𝑆 ) = { ( 𝐹 ‘ 𝑋 ) } ) )
33	9 32	mpd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 “ 𝑆 ) = { ( 𝐹 ‘ 𝑋 ) } )