Theorem preimane

Description: Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023)

	Ref	Expression
Hypotheses	preimane.f	⊢ ( 𝜑 → Fun 𝐹 )
	preimane.x	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
	preimane.y	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐹 )
	preimane.1	⊢ ( 𝜑 → 𝑌 ∈ ran 𝐹 )
Assertion	preimane	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ( ◡ 𝐹 “ { 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		preimane.f	⊢ ( 𝜑 → Fun 𝐹 )
2		preimane.x	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
3		preimane.y	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐹 )
4		preimane.1	⊢ ( 𝜑 → 𝑌 ∈ ran 𝐹 )
5		sneqrg	⊢ ( 𝑋 ∈ ran 𝐹 → ( { 𝑋 } = { 𝑌 } → 𝑋 = 𝑌 ) )
6	3 5	syl	⊢ ( 𝜑 → ( { 𝑋 } = { 𝑌 } → 𝑋 = 𝑌 ) )
7	6	necon3d	⊢ ( 𝜑 → ( 𝑋 ≠ 𝑌 → { 𝑋 } ≠ { 𝑌 } ) )
8	2 7	mpd	⊢ ( 𝜑 → { 𝑋 } ≠ { 𝑌 } )
9		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑋 } ) ) = ( { 𝑋 } ∩ ran 𝐹 ) )
10	1 9	syl	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑋 } ) ) = ( { 𝑋 } ∩ ran 𝐹 ) )
11	3	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ ran 𝐹 )
12		dfss2	⊢ ( { 𝑋 } ⊆ ran 𝐹 ↔ ( { 𝑋 } ∩ ran 𝐹 ) = { 𝑋 } )
13	11 12	sylib	⊢ ( 𝜑 → ( { 𝑋 } ∩ ran 𝐹 ) = { 𝑋 } )
14	10 13	eqtrd	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑋 } ) ) = { 𝑋 } )
15		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑌 } ) ) = ( { 𝑌 } ∩ ran 𝐹 ) )
16	1 15	syl	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑌 } ) ) = ( { 𝑌 } ∩ ran 𝐹 ) )
17	4	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ ran 𝐹 )
18		dfss2	⊢ ( { 𝑌 } ⊆ ran 𝐹 ↔ ( { 𝑌 } ∩ ran 𝐹 ) = { 𝑌 } )
19	17 18	sylib	⊢ ( 𝜑 → ( { 𝑌 } ∩ ran 𝐹 ) = { 𝑌 } )
20	16 19	eqtrd	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑌 } ) ) = { 𝑌 } )
21	8 14 20	3netr4d	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑋 } ) ) ≠ ( 𝐹 “ ( ◡ 𝐹 “ { 𝑌 } ) ) )
22		imaeq2	⊢ ( ( ◡ 𝐹 “ { 𝑋 } ) = ( ◡ 𝐹 “ { 𝑌 } ) → ( 𝐹 “ ( ◡ 𝐹 “ { 𝑋 } ) ) = ( 𝐹 “ ( ◡ 𝐹 “ { 𝑌 } ) ) )
23	22	necon3i	⊢ ( ( 𝐹 “ ( ◡ 𝐹 “ { 𝑋 } ) ) ≠ ( 𝐹 “ ( ◡ 𝐹 “ { 𝑌 } ) ) → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ( ◡ 𝐹 “ { 𝑌 } ) )
24	21 23	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ( ◡ 𝐹 “ { 𝑌 } ) )