| Step | Hyp | Ref
| Expression |
| 1 | | difss 4136 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ ((𝐺 ∘ 𝐹) ∘ ◡𝐺) |
| 2 | | dmss 5913 |
. . . . . 6
⊢ ((((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ ((𝐺 ∘ 𝐹) ∘ ◡𝐺) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ dom ((𝐺 ∘ 𝐹) ∘ ◡𝐺)) |
| 3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ dom
(((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ dom ((𝐺 ∘ 𝐹) ∘ ◡𝐺) |
| 4 | | dmcoss 5985 |
. . . . 5
⊢ dom
((𝐺 ∘ 𝐹) ∘ ◡𝐺) ⊆ dom ◡𝐺 |
| 5 | 3, 4 | sstri 3993 |
. . . 4
⊢ dom
(((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ dom ◡𝐺 |
| 6 | | f1ocnv 6860 |
. . . . . 6
⊢ (𝐺:𝐴–1-1-onto→𝐴 → ◡𝐺:𝐴–1-1-onto→𝐴) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ◡𝐺:𝐴–1-1-onto→𝐴) |
| 8 | | f1odm 6852 |
. . . . 5
⊢ (◡𝐺:𝐴–1-1-onto→𝐴 → dom ◡𝐺 = 𝐴) |
| 9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom ◡𝐺 = 𝐴) |
| 10 | 5, 9 | sseqtrid 4026 |
. . 3
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ⊆ 𝐴) |
| 11 | 10 | sselda 3983 |
. 2
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I )) → 𝑥 ∈ 𝐴) |
| 12 | | imassrn 6089 |
. . . 4
⊢ (𝐺 “ dom (𝐹 ∖ I )) ⊆ ran 𝐺 |
| 13 | | f1of 6848 |
. . . . . 6
⊢ (𝐺:𝐴–1-1-onto→𝐴 → 𝐺:𝐴⟶𝐴) |
| 14 | 13 | adantl 481 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → 𝐺:𝐴⟶𝐴) |
| 15 | 14 | frnd 6744 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ran 𝐺 ⊆ 𝐴) |
| 16 | 12, 15 | sstrid 3995 |
. . 3
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → (𝐺 “ dom (𝐹 ∖ I )) ⊆ 𝐴) |
| 17 | 16 | sselda 3983 |
. 2
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I ))) → 𝑥 ∈ 𝐴) |
| 18 | | simpl 482 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → 𝐹:𝐴⟶𝐴) |
| 19 | | fco 6760 |
. . . . . . 7
⊢ ((𝐺:𝐴⟶𝐴 ∧ 𝐹:𝐴⟶𝐴) → (𝐺 ∘ 𝐹):𝐴⟶𝐴) |
| 20 | 14, 18, 19 | syl2anc 584 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → (𝐺 ∘ 𝐹):𝐴⟶𝐴) |
| 21 | | f1of 6848 |
. . . . . . 7
⊢ (◡𝐺:𝐴–1-1-onto→𝐴 → ◡𝐺:𝐴⟶𝐴) |
| 22 | 7, 21 | syl 17 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ◡𝐺:𝐴⟶𝐴) |
| 23 | | fco 6760 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐹):𝐴⟶𝐴 ∧ ◡𝐺:𝐴⟶𝐴) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺):𝐴⟶𝐴) |
| 24 | 20, 22, 23 | syl2anc 584 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺):𝐴⟶𝐴) |
| 25 | 24 | ffnd 6737 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) Fn 𝐴) |
| 26 | | fnelnfp 7197 |
. . . 4
⊢ ((((𝐺 ∘ 𝐹) ∘ ◡𝐺) Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ↔ (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) ≠ 𝑥)) |
| 27 | 25, 26 | sylan 580 |
. . 3
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ↔ (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) ≠ 𝑥)) |
| 28 | | f1ofn 6849 |
. . . . . . . . 9
⊢ (◡𝐺:𝐴–1-1-onto→𝐴 → ◡𝐺 Fn 𝐴) |
| 29 | 7, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → ◡𝐺 Fn 𝐴) |
| 30 | | fvco2 7006 |
. . . . . . . 8
⊢ ((◡𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥))) |
| 31 | 29, 30 | sylan 580 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥))) |
| 32 | | ffn 6736 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐴 → 𝐹 Fn 𝐴) |
| 33 | 32 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn 𝐴) |
| 34 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((◡𝐺:𝐴⟶𝐴 ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘𝑥) ∈ 𝐴) |
| 35 | 22, 34 | sylan 580 |
. . . . . . . 8
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘𝑥) ∈ 𝐴) |
| 36 | | fvco2 7006 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥)) = (𝐺‘(𝐹‘(◡𝐺‘𝑥)))) |
| 37 | 33, 35, 36 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘(◡𝐺‘𝑥)) = (𝐺‘(𝐹‘(◡𝐺‘𝑥)))) |
| 38 | 31, 37 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = (𝐺‘(𝐹‘(◡𝐺‘𝑥)))) |
| 39 | 38 | eqeq1d 2739 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = 𝑥 ↔ (𝐺‘(𝐹‘(◡𝐺‘𝑥))) = 𝑥)) |
| 40 | | simplr 769 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐺:𝐴–1-1-onto→𝐴) |
| 41 | | simpll 767 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐹:𝐴⟶𝐴) |
| 42 | | ffvelcdm 7101 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴) → (𝐹‘(◡𝐺‘𝑥)) ∈ 𝐴) |
| 43 | 41, 35, 42 | syl2anc 584 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝐹‘(◡𝐺‘𝑥)) ∈ 𝐴) |
| 44 | | simpr 484 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 45 | | f1ocnvfvb 7299 |
. . . . . 6
⊢ ((𝐺:𝐴–1-1-onto→𝐴 ∧ (𝐹‘(◡𝐺‘𝑥)) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(𝐹‘(◡𝐺‘𝑥))) = 𝑥 ↔ (◡𝐺‘𝑥) = (𝐹‘(◡𝐺‘𝑥)))) |
| 46 | 40, 43, 44, 45 | syl3anc 1373 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(𝐹‘(◡𝐺‘𝑥))) = 𝑥 ↔ (◡𝐺‘𝑥) = (𝐹‘(◡𝐺‘𝑥)))) |
| 47 | 39, 46 | bitrd 279 |
. . . 4
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) = 𝑥 ↔ (◡𝐺‘𝑥) = (𝐹‘(◡𝐺‘𝑥)))) |
| 48 | 47 | necon3bid 2985 |
. . 3
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((((𝐺 ∘ 𝐹) ∘ ◡𝐺)‘𝑥) ≠ 𝑥 ↔ (◡𝐺‘𝑥) ≠ (𝐹‘(◡𝐺‘𝑥)))) |
| 49 | | necom 2994 |
. . . 4
⊢ ((◡𝐺‘𝑥) ≠ (𝐹‘(◡𝐺‘𝑥)) ↔ (𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥)) |
| 50 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐺:𝐴–1-1-onto→𝐴 → 𝐺:𝐴–1-1→𝐴) |
| 51 | 50 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐺:𝐴–1-1→𝐴) |
| 52 | | difss 4136 |
. . . . . . . . 9
⊢ (𝐹 ∖ I ) ⊆ 𝐹 |
| 53 | | dmss 5913 |
. . . . . . . . 9
⊢ ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹) |
| 54 | 52, 53 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ I ) ⊆ dom
𝐹 |
| 55 | | fdm 6745 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐴 → dom 𝐹 = 𝐴) |
| 56 | 54, 55 | sseqtrid 4026 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐴 → dom (𝐹 ∖ I ) ⊆ 𝐴) |
| 57 | 56 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → dom (𝐹 ∖ I ) ⊆ 𝐴) |
| 58 | | f1elima 7283 |
. . . . . 6
⊢ ((𝐺:𝐴–1-1→𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴 ∧ dom (𝐹 ∖ I ) ⊆ 𝐴) → ((𝐺‘(◡𝐺‘𝑥)) ∈ (𝐺 “ dom (𝐹 ∖ I )) ↔ (◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ))) |
| 59 | 51, 35, 57, 58 | syl3anc 1373 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘𝑥)) ∈ (𝐺 “ dom (𝐹 ∖ I )) ↔ (◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ))) |
| 60 | | f1ocnvfv2 7297 |
. . . . . . 7
⊢ ((𝐺:𝐴–1-1-onto→𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥) |
| 61 | 60 | adantll 714 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥) |
| 62 | 61 | eleq1d 2826 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘𝑥)) ∈ (𝐺 “ dom (𝐹 ∖ I )) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
| 63 | | fnelnfp 7197 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ (◡𝐺‘𝑥) ∈ 𝐴) → ((◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥))) |
| 64 | 33, 35, 63 | syl2anc 584 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘𝑥) ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥))) |
| 65 | 59, 62, 64 | 3bitr3rd 310 |
. . . 4
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘(◡𝐺‘𝑥)) ≠ (◡𝐺‘𝑥) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
| 66 | 49, 65 | bitrid 283 |
. . 3
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘𝑥) ≠ (𝐹‘(◡𝐺‘𝑥)) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
| 67 | 27, 48, 66 | 3bitrd 305 |
. 2
⊢ (((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) ↔ 𝑥 ∈ (𝐺 “ dom (𝐹 ∖ I )))) |
| 68 | 11, 17, 67 | eqrdav 2736 |
1
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) = (𝐺 “ dom (𝐹 ∖ I ))) |