Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ≈ 𝐵) |
2 | | bren 8576 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑠 𝑠:𝐴–1-1-onto→𝐵) |
3 | 1, 2 | sylib 221 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ∃𝑠 𝑠:𝐴–1-1-onto→𝐵) |
4 | | deranglem 32711 |
. . . . 5
⊢ (𝐵 ∈ Fin → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) |
5 | 4 | adantl 485 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) |
6 | | f1oco 6652 |
. . . . . . . . . . . 12
⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐴–1-1-onto→𝐴) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵) |
7 | 6 | ad2ant2lr 748 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵) |
8 | | f1ocnv 6642 |
. . . . . . . . . . . 12
⊢ (𝑠:𝐴–1-1-onto→𝐵 → ◡𝑠:𝐵–1-1-onto→𝐴) |
9 | 8 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ◡𝑠:𝐵–1-1-onto→𝐴) |
10 | | f1oco 6652 |
. . . . . . . . . . 11
⊢ (((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 ∧ ◡𝑠:𝐵–1-1-onto→𝐴) → ((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵) |
11 | 7, 9, 10 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵) |
12 | | coass 6108 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∘ 𝑔) ∘ ◡𝑠) = (𝑠 ∘ (𝑔 ∘ ◡𝑠)) |
13 | 12 | fveq1i 6687 |
. . . . . . . . . . . . . 14
⊢ (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) = ((𝑠 ∘ (𝑔 ∘ ◡𝑠))‘𝑧) |
14 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → 𝑔:𝐴–1-1-onto→𝐴) |
15 | | f1oco 6652 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ◡𝑠:𝐵–1-1-onto→𝐴) → (𝑔 ∘ ◡𝑠):𝐵–1-1-onto→𝐴) |
16 | 14, 9, 15 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ◡𝑠):𝐵–1-1-onto→𝐴) |
17 | | f1of 6630 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∘ ◡𝑠):𝐵–1-1-onto→𝐴 → (𝑔 ∘ ◡𝑠):𝐵⟶𝐴) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ◡𝑠):𝐵⟶𝐴) |
19 | | fvco3 6779 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔 ∘ ◡𝑠):𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧))) |
20 | 18, 19 | sylan 583 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧))) |
21 | 13, 20 | syl5eq 2786 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) = (𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧))) |
22 | | f1of 6630 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑠:𝐵–1-1-onto→𝐴 → ◡𝑠:𝐵⟶𝐴) |
23 | 9, 22 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ◡𝑠:𝐵⟶𝐴) |
24 | | fvco3 6779 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑠:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ◡𝑠)‘𝑧) = (𝑔‘(◡𝑠‘𝑧))) |
25 | 23, 24 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ◡𝑠)‘𝑧) = (𝑔‘(◡𝑠‘𝑧))) |
26 | 23 | ffvelrnda 6873 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (◡𝑠‘𝑧) ∈ 𝐴) |
27 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) |
28 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (◡𝑠‘𝑧) → (𝑔‘𝑦) = (𝑔‘(◡𝑠‘𝑧))) |
29 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (◡𝑠‘𝑧) → 𝑦 = (◡𝑠‘𝑧)) |
30 | 28, 29 | neeq12d 2996 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (◡𝑠‘𝑧) → ((𝑔‘𝑦) ≠ 𝑦 ↔ (𝑔‘(◡𝑠‘𝑧)) ≠ (◡𝑠‘𝑧))) |
31 | 30 | rspcv 3524 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑠‘𝑧) ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦 → (𝑔‘(◡𝑠‘𝑧)) ≠ (◡𝑠‘𝑧))) |
32 | 26, 27, 31 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑔‘(◡𝑠‘𝑧)) ≠ (◡𝑠‘𝑧)) |
33 | 25, 32 | eqnetrd 3002 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ◡𝑠)‘𝑧) ≠ (◡𝑠‘𝑧)) |
34 | 33 | necomd 2990 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (◡𝑠‘𝑧) ≠ ((𝑔 ∘ ◡𝑠)‘𝑧)) |
35 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → 𝑠:𝐴–1-1-onto→𝐵) |
36 | 18 | ffvelrnda 6873 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ◡𝑠)‘𝑧) ∈ 𝐴) |
37 | | f1ocnvfv 7058 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ((𝑔 ∘ ◡𝑠)‘𝑧) ∈ 𝐴) → ((𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧)) = 𝑧 → (◡𝑠‘𝑧) = ((𝑔 ∘ ◡𝑠)‘𝑧))) |
38 | 35, 36, 37 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧)) = 𝑧 → (◡𝑠‘𝑧) = ((𝑔 ∘ ◡𝑠)‘𝑧))) |
39 | 38 | necon3d 2956 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((◡𝑠‘𝑧) ≠ ((𝑔 ∘ ◡𝑠)‘𝑧) → (𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧)) ≠ 𝑧)) |
40 | 34, 39 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑠‘((𝑔 ∘ ◡𝑠)‘𝑧)) ≠ 𝑧) |
41 | 21, 40 | eqnetrd 3002 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) ≠ 𝑧) |
42 | 41 | ralrimiva 3097 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) ≠ 𝑧) |
43 | | fveq2 6686 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) = (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦)) |
44 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) |
45 | 43, 44 | neeq12d 2996 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → ((((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) ≠ 𝑧 ↔ (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦)) |
46 | 45 | cbvralvw 3350 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦) |
47 | 42, 46 | sylib 221 |
. . . . . . . . . 10
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦) |
48 | 11, 47 | jca 515 |
. . . . . . . . 9
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦)) |
49 | 48 | ex 416 |
. . . . . . . 8
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦))) |
50 | | vex 3404 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
51 | | f1oeq1 6618 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝑓:𝐴–1-1-onto→𝐴 ↔ 𝑔:𝐴–1-1-onto→𝐴)) |
52 | | fveq1 6685 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓‘𝑦) = (𝑔‘𝑦)) |
53 | 52 | neeq1d 2994 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑔‘𝑦) ≠ 𝑦)) |
54 | 53 | ralbidv 3110 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) |
55 | 51, 54 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))) |
56 | 50, 55 | elab 3578 |
. . . . . . . 8
⊢ (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) |
57 | | vex 3404 |
. . . . . . . . . . 11
⊢ 𝑠 ∈ V |
58 | 57, 50 | coex 7673 |
. . . . . . . . . 10
⊢ (𝑠 ∘ 𝑔) ∈ V |
59 | 57 | cnvex 7668 |
. . . . . . . . . 10
⊢ ◡𝑠 ∈ V |
60 | 58, 59 | coex 7673 |
. . . . . . . . 9
⊢ ((𝑠 ∘ 𝑔) ∘ ◡𝑠) ∈ V |
61 | | f1oeq1 6618 |
. . . . . . . . . 10
⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ◡𝑠) → (𝑓:𝐵–1-1-onto→𝐵 ↔ ((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵)) |
62 | | fveq1 6685 |
. . . . . . . . . . . 12
⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ◡𝑠) → (𝑓‘𝑦) = (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦)) |
63 | 62 | neeq1d 2994 |
. . . . . . . . . . 11
⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ◡𝑠) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦)) |
64 | 63 | ralbidv 3110 |
. . . . . . . . . 10
⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ◡𝑠) → (∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦)) |
65 | 61, 64 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ◡𝑠) → ((𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦) ↔ (((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦))) |
66 | 60, 65 | elab 3578 |
. . . . . . . 8
⊢ (((𝑠 ∘ 𝑔) ∘ ◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ↔ (((𝑠 ∘ 𝑔) ∘ ◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ◡𝑠)‘𝑦) ≠ 𝑦)) |
67 | 49, 56, 66 | 3imtr4g 299 |
. . . . . . 7
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} → ((𝑠 ∘ 𝑔) ∘ ◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
68 | | vex 3404 |
. . . . . . . . . 10
⊢ ℎ ∈ V |
69 | | f1oeq1 6618 |
. . . . . . . . . . 11
⊢ (𝑓 = ℎ → (𝑓:𝐴–1-1-onto→𝐴 ↔ ℎ:𝐴–1-1-onto→𝐴)) |
70 | | fveq1 6685 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦)) |
71 | 70 | neeq1d 2994 |
. . . . . . . . . . . 12
⊢ (𝑓 = ℎ → ((𝑓‘𝑦) ≠ 𝑦 ↔ (ℎ‘𝑦) ≠ 𝑦)) |
72 | 71 | ralbidv 3110 |
. . . . . . . . . . 11
⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)) |
73 | 69, 72 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑓 = ℎ → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) |
74 | 68, 73 | elab 3578 |
. . . . . . . . 9
⊢ (ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)) |
75 | 56, 74 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ↔ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) |
76 | 8 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ◡𝑠:𝐵–1-1-onto→𝐴) |
77 | | f1ofo 6637 |
. . . . . . . . . . . 12
⊢ (◡𝑠:𝐵–1-1-onto→𝐴 → ◡𝑠:𝐵–onto→𝐴) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ◡𝑠:𝐵–onto→𝐴) |
79 | 7 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵) |
80 | | f1ofn 6631 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 → (𝑠 ∘ 𝑔) Fn 𝐴) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ 𝑔) Fn 𝐴) |
82 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑠:𝐴–1-1-onto→𝐵) |
83 | | simprrl 781 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴–1-1-onto→𝐴) |
84 | | f1oco 6652 |
. . . . . . . . . . . . 13
⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐴–1-1-onto→𝐴) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵) |
85 | 82, 83, 84 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵) |
86 | | f1ofn 6631 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵 → (𝑠 ∘ ℎ) Fn 𝐴) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ) Fn 𝐴) |
88 | | cocan2 7071 |
. . . . . . . . . . 11
⊢ ((◡𝑠:𝐵–onto→𝐴 ∧ (𝑠 ∘ 𝑔) Fn 𝐴 ∧ (𝑠 ∘ ℎ) Fn 𝐴) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠) = ((𝑠 ∘ ℎ) ∘ ◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ))) |
89 | 78, 81, 87, 88 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠) = ((𝑠 ∘ ℎ) ∘ ◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ))) |
90 | | f1of1 6629 |
. . . . . . . . . . . 12
⊢ (𝑠:𝐴–1-1-onto→𝐵 → 𝑠:𝐴–1-1→𝐵) |
91 | 90 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑠:𝐴–1-1→𝐵) |
92 | | simprll 779 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴–1-1-onto→𝐴) |
93 | | f1of 6630 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐴–1-1-onto→𝐴 → 𝑔:𝐴⟶𝐴) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴⟶𝐴) |
95 | | f1of 6630 |
. . . . . . . . . . . 12
⊢ (ℎ:𝐴–1-1-onto→𝐴 → ℎ:𝐴⟶𝐴) |
96 | 83, 95 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴⟶𝐴) |
97 | | cocan1 7070 |
. . . . . . . . . . 11
⊢ ((𝑠:𝐴–1-1→𝐵 ∧ 𝑔:𝐴⟶𝐴 ∧ ℎ:𝐴⟶𝐴) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ)) |
98 | 91, 94, 96, 97 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ)) |
99 | 89, 98 | bitrd 282 |
. . . . . . . . 9
⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠) = ((𝑠 ∘ ℎ) ∘ ◡𝑠) ↔ 𝑔 = ℎ)) |
100 | 99 | ex 416 |
. . . . . . . 8
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠) = ((𝑠 ∘ ℎ) ∘ ◡𝑠) ↔ 𝑔 = ℎ))) |
101 | 75, 100 | syl5bi 245 |
. . . . . . 7
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) → (((𝑠 ∘ 𝑔) ∘ ◡𝑠) = ((𝑠 ∘ ℎ) ∘ ◡𝑠) ↔ 𝑔 = ℎ))) |
102 | 67, 101 | dom2d 8608 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
103 | 102 | ex 416 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))) |
104 | 103 | exlimdv 1940 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (∃𝑠 𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))) |
105 | 3, 5, 104 | mp2d 49 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) |
106 | | enfii 8796 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) |
107 | 106 | ancoms 462 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
108 | | deranglem 32711 |
. . . . 5
⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) |
109 | 107, 108 | syl 17 |
. . . 4
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) |
110 | | hashdom 13844 |
. . . 4
⊢ (({𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin ∧ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) ↔ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
111 | 109, 5, 110 | syl2anc 587 |
. . 3
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) ↔ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
112 | 105, 111 | mpbird 260 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
113 | | derang.d |
. . . 4
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)})) |
114 | 113 | derangval 32712 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)})) |
115 | 107, 114 | syl 17 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)})) |
116 | 113 | derangval 32712 |
. . 3
⊢ (𝐵 ∈ Fin → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
117 | 116 | adantl 485 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})) |
118 | 112, 115,
117 | 3brtr4d 5072 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵)) |