Theorem preimafvelsetpreimafv

Description: The preimage of a function value is an element of the class P of all preimages of function values. (Contributed by AV, 10-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		id	⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐴 )
3		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
4	3	sneqd	⊢ ( 𝑥 = 𝑋 → { ( 𝐹 ‘ 𝑥 ) } = { ( 𝐹 ‘ 𝑋 ) } )
5	4	imaeq2d	⊢ ( 𝑥 = 𝑋 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )
6	5	eqeq2d	⊢ ( 𝑥 = 𝑋 → ( ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) )
7	6	adantl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑥 = 𝑋 ) → ( ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) )
8		eqidd	⊢ ( 𝑋 ∈ 𝐴 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )
9	2 7 8	rspcedvd	⊢ ( 𝑋 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
10	9	3ad2ant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
11		fnex	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
12		cnvexg	⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V )
13		imaexg	⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ V )
14	11 12 13	3syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ V )
15	14	3adant3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ V )
16	1	elsetpreimafvb	⊢ ( ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ V → ( ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
17	15 16	syl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
18	10 17	mpbird	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ∈ 𝑃 )