Description: Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | f1omvdconj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difss | |
|
2 | dmss | |
|
3 | 1 2 | ax-mp | |
4 | dmcoss | |
|
5 | 3 4 | sstri | |
6 | f1ocnv | |
|
7 | 6 | adantl | |
8 | f1odm | |
|
9 | 7 8 | syl | |
10 | 5 9 | sseqtrid | |
11 | 10 | sselda | |
12 | imassrn | |
|
13 | f1of | |
|
14 | 13 | adantl | |
15 | 14 | frnd | |
16 | 12 15 | sstrid | |
17 | 16 | sselda | |
18 | simpl | |
|
19 | fco | |
|
20 | 14 18 19 | syl2anc | |
21 | f1of | |
|
22 | 7 21 | syl | |
23 | fco | |
|
24 | 20 22 23 | syl2anc | |
25 | 24 | ffnd | |
26 | fnelnfp | |
|
27 | 25 26 | sylan | |
28 | f1ofn | |
|
29 | 7 28 | syl | |
30 | fvco2 | |
|
31 | 29 30 | sylan | |
32 | ffn | |
|
33 | 32 | ad2antrr | |
34 | ffvelrn | |
|
35 | 22 34 | sylan | |
36 | fvco2 | |
|
37 | 33 35 36 | syl2anc | |
38 | 31 37 | eqtrd | |
39 | 38 | eqeq1d | |
40 | simplr | |
|
41 | simpll | |
|
42 | ffvelrn | |
|
43 | 41 35 42 | syl2anc | |
44 | simpr | |
|
45 | f1ocnvfvb | |
|
46 | 40 43 44 45 | syl3anc | |
47 | 39 46 | bitrd | |
48 | 47 | necon3bid | |
49 | necom | |
|
50 | f1of1 | |
|
51 | 50 | ad2antlr | |
52 | difss | |
|
53 | dmss | |
|
54 | 52 53 | ax-mp | |
55 | fdm | |
|
56 | 54 55 | sseqtrid | |
57 | 56 | ad2antrr | |
58 | f1elima | |
|
59 | 51 35 57 58 | syl3anc | |
60 | f1ocnvfv2 | |
|
61 | 60 | adantll | |
62 | 61 | eleq1d | |
63 | fnelnfp | |
|
64 | 33 35 63 | syl2anc | |
65 | 59 62 64 | 3bitr3rd | |
66 | 49 65 | syl5bb | |
67 | 27 48 66 | 3bitrd | |
68 | 11 17 67 | eqrdav | |