Metamath Proof Explorer


Theorem f1omvdmvd

Description: A permutation of any class moves a point which is moved to a different point which is moved. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1omvdmvd F:A1-1 ontoAXdomFIFXdomFIX

Proof

Step Hyp Ref Expression
1 simpr F:A1-1 ontoAXdomFIXdomFI
2 f1ofn F:A1-1 ontoAFFnA
3 difss FIF
4 dmss FIFdomFIdomF
5 3 4 ax-mp domFIdomF
6 f1odm F:A1-1 ontoAdomF=A
7 5 6 sseqtrid F:A1-1 ontoAdomFIA
8 7 sselda F:A1-1 ontoAXdomFIXA
9 fnelnfp FFnAXAXdomFIFXX
10 2 8 9 syl2an2r F:A1-1 ontoAXdomFIXdomFIFXX
11 1 10 mpbid F:A1-1 ontoAXdomFIFXX
12 f1of1 F:A1-1 ontoAF:A1-1A
13 12 adantr F:A1-1 ontoAXdomFIF:A1-1A
14 f1of F:A1-1 ontoAF:AA
15 14 adantr F:A1-1 ontoAXdomFIF:AA
16 15 8 ffvelrnd F:A1-1 ontoAXdomFIFXA
17 f1fveq F:A1-1AFXAXAFFX=FXFX=X
18 13 16 8 17 syl12anc F:A1-1 ontoAXdomFIFFX=FXFX=X
19 18 necon3bid F:A1-1 ontoAXdomFIFFXFXFXX
20 11 19 mpbird F:A1-1 ontoAXdomFIFFXFX
21 fnelnfp FFnAFXAFXdomFIFFXFX
22 2 16 21 syl2an2r F:A1-1 ontoAXdomFIFXdomFIFFXFX
23 20 22 mpbird F:A1-1 ontoAXdomFIFXdomFI
24 eldifsn FXdomFIXFXdomFIFXX
25 23 11 24 sylanbrc F:A1-1 ontoAXdomFIFXdomFIX