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 ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) = ( 𝐺 “ dom ( 𝐹 ∖ I ) ) )

Proof

Step Hyp Ref Expression
1 difss ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ⊆ ( ( 𝐺𝐹 ) ∘ 𝐺 )
2 dmss ( ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ⊆ ( ( 𝐺𝐹 ) ∘ 𝐺 ) → dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ⊆ dom ( ( 𝐺𝐹 ) ∘ 𝐺 ) )
3 1 2 ax-mp dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ⊆ dom ( ( 𝐺𝐹 ) ∘ 𝐺 )
4 dmcoss dom ( ( 𝐺𝐹 ) ∘ 𝐺 ) ⊆ dom 𝐺
5 3 4 sstri dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ⊆ dom 𝐺
6 f1ocnv ( 𝐺 : 𝐴1-1-onto𝐴 𝐺 : 𝐴1-1-onto𝐴 )
7 6 adantl ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → 𝐺 : 𝐴1-1-onto𝐴 )
8 f1odm ( 𝐺 : 𝐴1-1-onto𝐴 → dom 𝐺 = 𝐴 )
9 7 8 syl ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → dom 𝐺 = 𝐴 )
10 5 9 sseqtrid ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ⊆ 𝐴 )
11 10 sselda ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥 ∈ dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ) → 𝑥𝐴 )
12 imassrn ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ⊆ ran 𝐺
13 f1of ( 𝐺 : 𝐴1-1-onto𝐴𝐺 : 𝐴𝐴 )
14 13 adantl ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → 𝐺 : 𝐴𝐴 )
15 14 frnd ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → ran 𝐺𝐴 )
16 12 15 sstrid ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ⊆ 𝐴 )
17 16 sselda ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ) → 𝑥𝐴 )
18 simpl ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → 𝐹 : 𝐴𝐴 )
19 fco ( ( 𝐺 : 𝐴𝐴𝐹 : 𝐴𝐴 ) → ( 𝐺𝐹 ) : 𝐴𝐴 )
20 14 18 19 syl2anc ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → ( 𝐺𝐹 ) : 𝐴𝐴 )
21 f1of ( 𝐺 : 𝐴1-1-onto𝐴 𝐺 : 𝐴𝐴 )
22 7 21 syl ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → 𝐺 : 𝐴𝐴 )
23 fco ( ( ( 𝐺𝐹 ) : 𝐴𝐴 𝐺 : 𝐴𝐴 ) → ( ( 𝐺𝐹 ) ∘ 𝐺 ) : 𝐴𝐴 )
24 20 22 23 syl2anc ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → ( ( 𝐺𝐹 ) ∘ 𝐺 ) : 𝐴𝐴 )
25 24 ffnd ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → ( ( 𝐺𝐹 ) ∘ 𝐺 ) Fn 𝐴 )
26 fnelnfp ( ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) Fn 𝐴𝑥𝐴 ) → ( 𝑥 ∈ dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ↔ ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) ≠ 𝑥 ) )
27 25 26 sylan ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ↔ ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) ≠ 𝑥 ) )
28 f1ofn ( 𝐺 : 𝐴1-1-onto𝐴 𝐺 Fn 𝐴 )
29 7 28 syl ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → 𝐺 Fn 𝐴 )
30 fvco2 ( ( 𝐺 Fn 𝐴𝑥𝐴 ) → ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝐺𝐹 ) ‘ ( 𝐺𝑥 ) ) )
31 29 30 sylan ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝐺𝐹 ) ‘ ( 𝐺𝑥 ) ) )
32 ffn ( 𝐹 : 𝐴𝐴𝐹 Fn 𝐴 )
33 32 ad2antrr ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → 𝐹 Fn 𝐴 )
34 ffvelrn ( ( 𝐺 : 𝐴𝐴𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ 𝐴 )
35 22 34 sylan ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ 𝐴 )
36 fvco2 ( ( 𝐹 Fn 𝐴 ∧ ( 𝐺𝑥 ) ∈ 𝐴 ) → ( ( 𝐺𝐹 ) ‘ ( 𝐺𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
37 33 35 36 syl2anc ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐺𝐹 ) ‘ ( 𝐺𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
38 31 37 eqtrd ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
39 38 eqeq1d ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) = 𝑥 ↔ ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) = 𝑥 ) )
40 simplr ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → 𝐺 : 𝐴1-1-onto𝐴 )
41 simpll ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → 𝐹 : 𝐴𝐴 )
42 ffvelrn ( ( 𝐹 : 𝐴𝐴 ∧ ( 𝐺𝑥 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑥 ) ) ∈ 𝐴 )
43 41 35 42 syl2anc ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( 𝐹 ‘ ( 𝐺𝑥 ) ) ∈ 𝐴 )
44 simpr ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → 𝑥𝐴 )
45 f1ocnvfvb ( ( 𝐺 : 𝐴1-1-onto𝐴 ∧ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ∈ 𝐴𝑥𝐴 ) → ( ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) = 𝑥 ↔ ( 𝐺𝑥 ) = ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
46 40 43 44 45 syl3anc ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐺 ‘ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) = 𝑥 ↔ ( 𝐺𝑥 ) = ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
47 39 46 bitrd ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) = 𝑥 ↔ ( 𝐺𝑥 ) = ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
48 47 necon3bid ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ‘ 𝑥 ) ≠ 𝑥 ↔ ( 𝐺𝑥 ) ≠ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ) )
49 necom ( ( 𝐺𝑥 ) ≠ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ↔ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ≠ ( 𝐺𝑥 ) )
50 f1of1 ( 𝐺 : 𝐴1-1-onto𝐴𝐺 : 𝐴1-1𝐴 )
51 50 ad2antlr ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → 𝐺 : 𝐴1-1𝐴 )
52 difss ( 𝐹 ∖ I ) ⊆ 𝐹
53 dmss ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
54 52 53 ax-mp dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
55 fdm ( 𝐹 : 𝐴𝐴 → dom 𝐹 = 𝐴 )
56 54 55 sseqtrid ( 𝐹 : 𝐴𝐴 → dom ( 𝐹 ∖ I ) ⊆ 𝐴 )
57 56 ad2antrr ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → dom ( 𝐹 ∖ I ) ⊆ 𝐴 )
58 f1elima ( ( 𝐺 : 𝐴1-1𝐴 ∧ ( 𝐺𝑥 ) ∈ 𝐴 ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐴 ) → ( ( 𝐺 ‘ ( 𝐺𝑥 ) ) ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ↔ ( 𝐺𝑥 ) ∈ dom ( 𝐹 ∖ I ) ) )
59 51 35 57 58 syl3anc ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐺 ‘ ( 𝐺𝑥 ) ) ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ↔ ( 𝐺𝑥 ) ∈ dom ( 𝐹 ∖ I ) ) )
60 f1ocnvfv2 ( ( 𝐺 : 𝐴1-1-onto𝐴𝑥𝐴 ) → ( 𝐺 ‘ ( 𝐺𝑥 ) ) = 𝑥 )
61 60 adantll ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( 𝐺 ‘ ( 𝐺𝑥 ) ) = 𝑥 )
62 61 eleq1d ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐺 ‘ ( 𝐺𝑥 ) ) ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ↔ 𝑥 ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ) )
63 fnelnfp ( ( 𝐹 Fn 𝐴 ∧ ( 𝐺𝑥 ) ∈ 𝐴 ) → ( ( 𝐺𝑥 ) ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ≠ ( 𝐺𝑥 ) ) )
64 33 35 63 syl2anc ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐺𝑥 ) ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ≠ ( 𝐺𝑥 ) ) )
65 59 62 64 3bitr3rd ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐹 ‘ ( 𝐺𝑥 ) ) ≠ ( 𝐺𝑥 ) ↔ 𝑥 ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ) )
66 49 65 syl5bb ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( ( 𝐺𝑥 ) ≠ ( 𝐹 ‘ ( 𝐺𝑥 ) ) ↔ 𝑥 ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ) )
67 27 48 66 3bitrd ( ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) ↔ 𝑥 ∈ ( 𝐺 “ dom ( 𝐹 ∖ I ) ) ) )
68 11 17 67 eqrdav ( ( 𝐹 : 𝐴𝐴𝐺 : 𝐴1-1-onto𝐴 ) → dom ( ( ( 𝐺𝐹 ) ∘ 𝐺 ) ∖ I ) = ( 𝐺 “ dom ( 𝐹 ∖ I ) ) )