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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | f1ofn | |
|
3 | difss | |
|
4 | dmss | |
|
5 | 3 4 | ax-mp | |
6 | f1odm | |
|
7 | 5 6 | sseqtrid | |
8 | 7 | sselda | |
9 | fnelnfp | |
|
10 | 2 8 9 | syl2an2r | |
11 | 1 10 | mpbid | |
12 | f1of1 | |
|
13 | 12 | adantr | |
14 | f1of | |
|
15 | 14 | adantr | |
16 | 15 8 | ffvelrnd | |
17 | f1fveq | |
|
18 | 13 16 8 17 | syl12anc | |
19 | 18 | necon3bid | |
20 | 11 19 | mpbird | |
21 | fnelnfp | |
|
22 | 2 16 21 | syl2an2r | |
23 | 20 22 | mpbird | |
24 | eldifsn | |
|
25 | 23 11 24 | sylanbrc | |