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