Metamath Proof Explorer


Theorem f1omvdconj

Description: Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1omvdconj F:AAG:A1-1 ontoAdomGFG-1I=GdomFI

Proof

Step Hyp Ref Expression
1 difss GFG-1IGFG-1
2 dmss GFG-1IGFG-1domGFG-1IdomGFG-1
3 1 2 ax-mp domGFG-1IdomGFG-1
4 dmcoss domGFG-1domG-1
5 3 4 sstri domGFG-1IdomG-1
6 f1ocnv G:A1-1 ontoAG-1:A1-1 ontoA
7 6 adantl F:AAG:A1-1 ontoAG-1:A1-1 ontoA
8 f1odm G-1:A1-1 ontoAdomG-1=A
9 7 8 syl F:AAG:A1-1 ontoAdomG-1=A
10 5 9 sseqtrid F:AAG:A1-1 ontoAdomGFG-1IA
11 10 sselda F:AAG:A1-1 ontoAxdomGFG-1IxA
12 imassrn GdomFIranG
13 f1of G:A1-1 ontoAG:AA
14 13 adantl F:AAG:A1-1 ontoAG:AA
15 14 frnd F:AAG:A1-1 ontoAranGA
16 12 15 sstrid F:AAG:A1-1 ontoAGdomFIA
17 16 sselda F:AAG:A1-1 ontoAxGdomFIxA
18 simpl F:AAG:A1-1 ontoAF:AA
19 fco G:AAF:AAGF:AA
20 14 18 19 syl2anc F:AAG:A1-1 ontoAGF:AA
21 f1of G-1:A1-1 ontoAG-1:AA
22 7 21 syl F:AAG:A1-1 ontoAG-1:AA
23 fco GF:AAG-1:AAGFG-1:AA
24 20 22 23 syl2anc F:AAG:A1-1 ontoAGFG-1:AA
25 24 ffnd F:AAG:A1-1 ontoAGFG-1FnA
26 fnelnfp GFG-1FnAxAxdomGFG-1IGFG-1xx
27 25 26 sylan F:AAG:A1-1 ontoAxAxdomGFG-1IGFG-1xx
28 f1ofn G-1:A1-1 ontoAG-1FnA
29 7 28 syl F:AAG:A1-1 ontoAG-1FnA
30 fvco2 G-1FnAxAGFG-1x=GFG-1x
31 29 30 sylan F:AAG:A1-1 ontoAxAGFG-1x=GFG-1x
32 ffn F:AAFFnA
33 32 ad2antrr F:AAG:A1-1 ontoAxAFFnA
34 ffvelrn G-1:AAxAG-1xA
35 22 34 sylan F:AAG:A1-1 ontoAxAG-1xA
36 fvco2 FFnAG-1xAGFG-1x=GFG-1x
37 33 35 36 syl2anc F:AAG:A1-1 ontoAxAGFG-1x=GFG-1x
38 31 37 eqtrd F:AAG:A1-1 ontoAxAGFG-1x=GFG-1x
39 38 eqeq1d F:AAG:A1-1 ontoAxAGFG-1x=xGFG-1x=x
40 simplr F:AAG:A1-1 ontoAxAG:A1-1 ontoA
41 simpll F:AAG:A1-1 ontoAxAF:AA
42 ffvelrn F:AAG-1xAFG-1xA
43 41 35 42 syl2anc F:AAG:A1-1 ontoAxAFG-1xA
44 simpr F:AAG:A1-1 ontoAxAxA
45 f1ocnvfvb G:A1-1 ontoAFG-1xAxAGFG-1x=xG-1x=FG-1x
46 40 43 44 45 syl3anc F:AAG:A1-1 ontoAxAGFG-1x=xG-1x=FG-1x
47 39 46 bitrd F:AAG:A1-1 ontoAxAGFG-1x=xG-1x=FG-1x
48 47 necon3bid F:AAG:A1-1 ontoAxAGFG-1xxG-1xFG-1x
49 necom G-1xFG-1xFG-1xG-1x
50 f1of1 G:A1-1 ontoAG:A1-1A
51 50 ad2antlr F:AAG:A1-1 ontoAxAG:A1-1A
52 difss FIF
53 dmss FIFdomFIdomF
54 52 53 ax-mp domFIdomF
55 fdm F:AAdomF=A
56 54 55 sseqtrid F:AAdomFIA
57 56 ad2antrr F:AAG:A1-1 ontoAxAdomFIA
58 f1elima G:A1-1AG-1xAdomFIAGG-1xGdomFIG-1xdomFI
59 51 35 57 58 syl3anc F:AAG:A1-1 ontoAxAGG-1xGdomFIG-1xdomFI
60 f1ocnvfv2 G:A1-1 ontoAxAGG-1x=x
61 60 adantll F:AAG:A1-1 ontoAxAGG-1x=x
62 61 eleq1d F:AAG:A1-1 ontoAxAGG-1xGdomFIxGdomFI
63 fnelnfp FFnAG-1xAG-1xdomFIFG-1xG-1x
64 33 35 63 syl2anc F:AAG:A1-1 ontoAxAG-1xdomFIFG-1xG-1x
65 59 62 64 3bitr3rd F:AAG:A1-1 ontoAxAFG-1xG-1xxGdomFI
66 49 65 syl5bb F:AAG:A1-1 ontoAxAG-1xFG-1xxGdomFI
67 27 48 66 3bitrd F:AAG:A1-1 ontoAxAxdomGFG-1IxGdomFI
68 11 17 67 eqrdav F:AAG:A1-1 ontoAdomGFG-1I=GdomFI