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 ) ) )