Metamath Proof Explorer


Theorem preimane

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

Ref Expression
Hypotheses preimane.f φFunF
preimane.x φXY
preimane.y φXranF
preimane.1 φYranF
Assertion preimane φF-1XF-1Y

Proof

Step Hyp Ref Expression
1 preimane.f φFunF
2 preimane.x φXY
3 preimane.y φXranF
4 preimane.1 φYranF
5 sneqrg XranFX=YX=Y
6 3 5 syl φX=YX=Y
7 6 necon3d φXYXY
8 2 7 mpd φXY
9 funimacnv FunFFF-1X=XranF
10 1 9 syl φFF-1X=XranF
11 3 snssd φXranF
12 df-ss XranFXranF=X
13 11 12 sylib φXranF=X
14 10 13 eqtrd φFF-1X=X
15 funimacnv FunFFF-1Y=YranF
16 1 15 syl φFF-1Y=YranF
17 4 snssd φYranF
18 df-ss YranFYranF=Y
19 17 18 sylib φYranF=Y
20 16 19 eqtrd φFF-1Y=Y
21 8 14 20 3netr4d φFF-1XFF-1Y
22 imaeq2 F-1X=F-1YFF-1X=FF-1Y
23 22 necon3i FF-1XFF-1YF-1XF-1Y
24 21 23 syl φF-1XF-1Y