Theorem fvelsetpreimafv

Description: There is an element in a preimage S of function values so that S is the preimage of the function value at this element. (Contributed by AV, 8-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		preimafvsnel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
3	2	adantrr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
4		eleq2	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
5	4	ad2antll	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) → ( 𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
6	3 5	mpbird	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) → 𝑥 ∈ 𝑆 )
7		simprr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) → 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
8	6 7	jca	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) → ( 𝑥 ∈ 𝑆 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
9	8	ex	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) → ( 𝑥 ∈ 𝑆 ∧ 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) )
10	9	reximdv2	⊢ ( 𝐹 Fn 𝐴 → ( ∃ 𝑥 ∈ 𝐴 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ∃ 𝑥 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
11	1	elsetpreimafv	⊢ ( 𝑆 ∈ 𝑃 → ∃ 𝑥 ∈ 𝐴 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
12	10 11	impel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ) → ∃ 𝑥 ∈ 𝑆 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )