Step | Hyp | Ref
| Expression |
1 | | difss 3699 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ ((𝐺 ∘ 𝐹) ∘ ◡𝐺) |
2 | | dmss 5245 |
. . . . . 6
⊢ ((((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ ((𝐺 ∘ 𝐹) ∘ ◡𝐺) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ dom ((𝐺 ∘ 𝐹) ∘ ◡𝐺)) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ dom
(((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ dom ((𝐺 ∘ 𝐹) ∘ ◡𝐺) |
4 | | dmcoss 5306 |
. . . . 5
⊢ dom
((𝐺 ∘ 𝐹) ∘ ◡𝐺) ⊆ dom ◡𝐺 |
5 | 3, 4 | sstri 3577 |
. . . 4
⊢ dom
(((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ dom ◡𝐺 |
6 | | f1ocnv 6062 |
. . . . . 6
⊢ (𝐺:𝐴–1-1-onto→𝐴 → ◡𝐺:𝐴–1-1-onto→𝐴) |
7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ◡𝐺:𝐴–1-1-onto→𝐴) |
8 | | f1odm 6054 |
. . . . 5
⊢ (◡𝐺:𝐴–1-1-onto→𝐴 → dom ◡𝐺 = 𝐴) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom ◡𝐺 = 𝐴) |
10 | 5, 9 | syl5sseq 3616 |
. . 3
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ 𝐴) |
11 | 10 | sselda 3568 |
. 2
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I )) → 𝑥 ∈ 𝐴) |
12 | | imassrn 5396 |
. . . 4
⊢ (𝐺 “ dom (𝐹 ∖ I )) ⊆ ran 𝐺 |
13 | | f1of 6050 |
. . . . . 6
⊢ (𝐺:𝐴–1-1-onto→𝐴 → 𝐺:𝐴⟶𝐴) |
14 | 13 | adantl 481 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → 𝐺:𝐴⟶𝐴) |
15 | | frn 5966 |
. . . . 5
⊢ (𝐺:𝐴⟶𝐴 → ran 𝐺 ⊆ 𝐴) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ran 𝐺 ⊆ 𝐴) |
17 | 12, 16 | syl5ss 3579 |
. . 3
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → (𝐺 “ dom (𝐹 ∖ I )) ⊆ 𝐴) |
18 | 17 | sselda 3568 |
. 2
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I ))) → 𝑥 ∈ 𝐴) |
19 | | simpl 472 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → 𝐹:𝐴⟶𝐴) |
20 | | fco 5971 |
. . . . . . 7
⊢ ((𝐺:𝐴⟶𝐴 ∧ 𝐹:𝐴⟶𝐴) → (𝐺 ∘ 𝐹):𝐴⟶𝐴) |
21 | 14, 19, 20 | syl2anc 691 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → (𝐺 ∘ 𝐹):𝐴⟶𝐴) |
22 | | f1of 6050 |
. . . . . . 7
⊢ (◡𝐺:𝐴–1-1-onto→𝐴 → ◡𝐺:𝐴⟶𝐴) |
23 | 7, 22 | syl 17 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ◡𝐺:𝐴⟶𝐴) |
24 | | fco 5971 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐹):𝐴⟶𝐴 ∧ ◡𝐺:𝐴⟶𝐴) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺):𝐴⟶𝐴) |
25 | 21, 23, 24 | syl2anc 691 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺):𝐴⟶𝐴) |
26 | | ffn 5958 |
. . . . 5
⊢ (((𝐺 ∘ 𝐹) ∘ ◡𝐺):𝐴⟶𝐴 → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) Fn 𝐴) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) Fn 𝐴) |
28 | | fnelnfp 6348 |
. . . 4
⊢ ((((𝐺 ∘ 𝐹) ∘ ◡𝐺) Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ↔ (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) ≠ 𝑥)) |
29 | 27, 28 | sylan 487 |
. . 3
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ↔ (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) ≠ 𝑥)) |
30 | | f1ofn 6051 |
. . . . . . . . 9
⊢ (◡𝐺:𝐴–1-1-onto→𝐴 → ◡𝐺 Fn 𝐴) |
31 | 7, 30 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ◡𝐺 Fn 𝐴) |
32 | | fvco2 6183 |
. . . . . . . 8
⊢ ((◡𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥))) |
33 | 31, 32 | sylan 487 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥))) |
34 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐴 → 𝐹 Fn 𝐴) |
35 | 34 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn 𝐴) |
36 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ ((◡𝐺:𝐴⟶𝐴 ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘𝑥) ∈ 𝐴) |
37 | 23, 36 | sylan 487 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘𝑥) ∈ 𝐴) |
38 | | fvco2 6183 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥)) = (𝐺‘(𝐹‘(◡𝐺‘𝑥)))) |
39 | 35, 37, 38 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥)) = (𝐺‘(𝐹‘(◡𝐺‘𝑥)))) |
40 | 33, 39 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = (𝐺‘(𝐹‘(◡𝐺‘𝑥)))) |
41 | 40 | eqeq1d 2612 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = 𝑥 ↔ (𝐺‘(𝐹‘(◡𝐺‘𝑥))) = 𝑥)) |
42 | | simplr 788 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐺:𝐴–1-1-onto→𝐴) |
43 | | simpll 786 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐹:𝐴⟶𝐴) |
44 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴) → (𝐹‘(◡𝐺‘𝑥)) ∈ 𝐴) |
45 | 43, 37, 44 | syl2anc 691 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(◡𝐺‘𝑥)) ∈ 𝐴) |
46 | | simpr 476 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
47 | | f1ocnvfvb 6435 |
. . . . . 6
⊢ ((𝐺:𝐴–1-1-onto→𝐴 ∧ (𝐹‘(◡𝐺‘𝑥)) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(𝐹‘(◡𝐺‘𝑥))) = 𝑥 ↔ (◡𝐺‘𝑥) = (𝐹‘(◡𝐺‘𝑥)))) |
48 | 42, 45, 46, 47 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(𝐹‘(◡𝐺‘𝑥))) = 𝑥 ↔ (◡𝐺‘𝑥) = (𝐹‘(◡𝐺‘𝑥)))) |
49 | 41, 48 | bitrd 267 |
. . . 4
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = 𝑥 ↔ (◡𝐺‘𝑥) = (𝐹‘(◡𝐺‘𝑥)))) |
50 | 49 | necon3bid 2826 |
. . 3
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) ≠ 𝑥 ↔ (◡𝐺‘𝑥) ≠ (𝐹‘(◡𝐺‘𝑥)))) |
51 | | necom 2835 |
. . . 4
⊢ ((◡𝐺‘𝑥) ≠ (𝐹‘(◡𝐺‘𝑥)) ↔ (𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥)) |
52 | | f1of1 6049 |
. . . . . . 7
⊢ (𝐺:𝐴–1-1-onto→𝐴 → 𝐺:𝐴–1-1→𝐴) |
53 | 52 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐺:𝐴–1-1→𝐴) |
54 | | difss 3699 |
. . . . . . . . 9
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
55 | | dmss 5245 |
. . . . . . . . 9
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
57 | | fdm 5964 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐴 → dom 𝐹 = 𝐴) |
58 | 56, 57 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐴 → dom (𝐹 ∖ I ) ⊆ 𝐴) |
59 | 58 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → dom (𝐹 ∖ I ) ⊆ 𝐴) |
60 | | f1elima 6421 |
. . . . . 6
⊢ ((𝐺:𝐴–1-1→𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴 ∧ dom (𝐹 ∖ I ) ⊆ 𝐴) → ((𝐺‘(◡𝐺‘𝑥)) ∈ (𝐺 “ dom (𝐹 ∖ I )) ↔ (◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ))) |
61 | 53, 37, 59, 60 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘𝑥)) ∈ (𝐺 “ dom (𝐹 ∖ I )) ↔ (◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ))) |
62 | | f1ocnvfv2 6433 |
. . . . . . 7
⊢ ((𝐺:𝐴–1-1-onto→𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥) |
63 | 62 | adantll 746 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥) |
64 | 63 | eleq1d 2672 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘𝑥)) ∈ (𝐺 “ dom (𝐹 ∖ I )) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
65 | | fnelnfp 6348 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴) → ((◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥))) |
66 | 35, 37, 65 | syl2anc 691 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥))) |
67 | 61, 64, 66 | 3bitr3rd 298 |
. . . 4
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
68 | 51, 67 | syl5bb 271 |
. . 3
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘𝑥) ≠ (𝐹‘(◡𝐺‘𝑥)) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
69 | 29, 50, 68 | 3bitrd 293 |
. 2
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
70 | 11, 18, 69 | eqrdav 2609 |
1
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) = (𝐺 “ dom (𝐹 ∖ I ))) |