Metamath Proof Explorer


Theorem preimane

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

Ref Expression
Hypotheses preimane.f φ Fun F
preimane.x φ X Y
preimane.y φ X ran F
preimane.1 φ Y ran F
Assertion preimane φ F -1 X F -1 Y

Proof

Step Hyp Ref Expression
1 preimane.f φ Fun F
2 preimane.x φ X Y
3 preimane.y φ X ran F
4 preimane.1 φ Y ran F
5 sneqrg X ran F X = Y X = Y
6 3 5 syl φ X = Y X = Y
7 6 necon3d φ X Y X Y
8 2 7 mpd φ X Y
9 funimacnv Fun F F F -1 X = X ran F
10 1 9 syl φ F F -1 X = X ran F
11 3 snssd φ X ran F
12 df-ss X ran F X ran F = X
13 11 12 sylib φ X ran F = X
14 10 13 eqtrd φ F F -1 X = X
15 funimacnv Fun F F F -1 Y = Y ran F
16 1 15 syl φ F F -1 Y = Y ran F
17 4 snssd φ Y ran F
18 df-ss Y ran F Y ran F = Y
19 17 18 sylib φ Y ran F = Y
20 16 19 eqtrd φ F F -1 Y = Y
21 8 14 20 3netr4d φ F F -1 X F F -1 Y
22 imaeq2 F -1 X = F -1 Y F F -1 X = F F -1 Y
23 22 necon3i F F -1 X F F -1 Y F -1 X F -1 Y
24 21 23 syl φ F -1 X F -1 Y