Theorem elsetpreimafvbi

Description: An element of the preimage of a function value is an element of the domain of the function with the same value as another element of the preimage. (Contributed by AV, 9-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
3		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
4		eqeq2	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) )
5	4	anbi2d	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
6	5	eqcoms	⊢ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
7	3 6	sylan9bb	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
8	7	ex	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑥 ) → ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) )
9	8	adantld	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) )
10	2 9	sylbid	⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) )
11		eleq2	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝑋 ∈ 𝑆 ↔ 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
12		eleq2	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝑌 ∈ 𝑆 ↔ 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
13	12	bibi1d	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ↔ ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) )
14	11 13	imbi12d	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( ( 𝑋 ∈ 𝑆 → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) ↔ ( 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝑌 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
15	10 14	syl5ibr	⊢ ( 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ 𝑆 → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
16	15	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ 𝑆 → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
17	1	elsetpreimafv	⊢ ( 𝑆 ∈ 𝑃 → ∃ 𝑥 ∈ 𝐴 𝑆 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
18	16 17	syl11	⊢ ( 𝐹 Fn 𝐴 → ( 𝑆 ∈ 𝑃 → ( 𝑋 ∈ 𝑆 → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
19	18	3imp	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) ) )