derangenlem - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > derangenlem		Structured version Visualization version GIF version

Theorem derangenlem 35663

Description: One half of derangen 35664. (Contributed by Mario Carneiro, 22-Jan-2015.)

**Hypothesis**
Ref	Expression
derang.d	⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))

**Assertion**
Ref	Expression
derangenlem	⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))

Distinct variable groups: 𝑥,𝑓,𝑦,𝐴 𝐵,𝑓,𝑥,𝑦 Allowed substitution hints: 𝐷(𝑥,𝑦,𝑓)

Proof of Theorem derangenlem Dummy variables 𝑔 ℎ 𝑠 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bren 8949	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
2	1	birani 508	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
3		deranglem 35658	. . . . 5 ⊢ (𝐵 ∈ Fin → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	3	adantl 486	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
5		f1oco 6844	. . . . . . . . . . . 12 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐴–1-1-onto→𝐴) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵)
6	5	ad2ant2lr 760	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵)
7		f1ocnv 6833	. . . . . . . . . . . 12 ⊢ (𝑠:𝐴–1-1-onto→𝐵 → ^◡𝑠:𝐵–1-1-onto→𝐴)
8	7	ad2antlr 739	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵–1-1-onto→𝐴)
9		f1oco 6844	. . . . . . . . . . 11 ⊢ (((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 ∧ ^◡𝑠:𝐵–1-1-onto→𝐴) → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵)
10	6, 8, 9	syl2anc 595	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵)
11		coass 6267	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = (𝑠 ∘ (𝑔 ∘ ^◡𝑠))
12	11	fveq1i 6882	. . . . . . . . . . . . . 14 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧)
13		simprl 782	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → 𝑔:𝐴–1-1-onto→𝐴)
14		f1oco 6844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ^◡𝑠:𝐵–1-1-onto→𝐴) → (𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴)
15	13, 8, 14	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴)
16		f1of 6820	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴 → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
17	15, 16	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
18		fvco3 6981	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ ^◡𝑠):𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
19	17, 18	sylan 591	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
20	12, 19	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
21		f1of 6820	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑠:𝐵–1-1-onto→𝐴 → ^◡𝑠:𝐵⟶𝐴)
22	8, 21	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵⟶𝐴)
23		fvco3 6981	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
24	22, 23	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
25	22	ffvelcdmda 7079	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ∈ 𝐴)
26		simplrr 789	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)
27		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → (𝑔‘𝑦) = (𝑔‘(^◡𝑠‘𝑧)))
28		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → 𝑦 = (^◡𝑠‘𝑧))
29	27, 28	neeq12d 3019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (^◡𝑠‘𝑧) → ((𝑔‘𝑦) ≠ 𝑦 ↔ (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
30	29	rspcv 3577	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠‘𝑧) ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦 → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
31	25, 26, 30	sylc 66	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧))
32	24, 31	eqnetrd 3025	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ≠ (^◡𝑠‘𝑧))
33	32	necomd 3013	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ≠ ((𝑔 ∘ ^◡𝑠)‘𝑧))
34		simpllr 787	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → 𝑠:𝐴–1-1-onto→𝐵)
35	17	ffvelcdmda 7079	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴)
36		f1ocnvfv 7276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
37	34, 35, 36	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
38	37	necon3d 2979	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((^◡𝑠‘𝑧) ≠ ((𝑔 ∘ ^◡𝑠)‘𝑧) → (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) ≠ 𝑧))
39	33, 38	mpd 16	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) ≠ 𝑧)
40	20, 39	eqnetrd 3025	. . . . . . . . . . . 12 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
41	40	ralrimiva 3157	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
42		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
43		id 23	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
44	42, 43	neeq12d 3019	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
45	44	cbvralvw 3243	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)
46	41, 45	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)
47	10, 46	jca 520	. . . . . . . . 9 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
48	47	ex 417	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
49		vex 3459	. . . . . . . . 9 ⊢ 𝑔 ∈ V
50		f1oeq1 6808	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓:𝐴–1-1-onto→𝐴 ↔ 𝑔:𝐴–1-1-onto→𝐴))
51		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑦) = (𝑔‘𝑦))
52	51	neeq1d 3017	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑔‘𝑦) ≠ 𝑦))
53	52	ralbidv 3188	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
54	50, 53	anbi12d 643	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)))
55	49, 54	elab 3638	. . . . . . . 8 ⊢ (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
56		vex 3459	. . . . . . . . . . 11 ⊢ 𝑠 ∈ V
57	56, 49	coex 7923	. . . . . . . . . 10 ⊢ (𝑠 ∘ 𝑔) ∈ V
58	56	cnvex 7918	. . . . . . . . . 10 ⊢ ^◡𝑠 ∈ V
59	57, 58	coex 7923	. . . . . . . . 9 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ V
60		f1oeq1 6808	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓:𝐵–1-1-onto→𝐵 ↔ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵))
61		fveq1 6880	. . . . . . . . . . . 12 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓‘𝑦) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
62	61	neeq1d 3017	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
63	62	ralbidv 3188	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
64	60, 63	anbi12d 643	. . . . . . . . 9 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦) ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
65	59, 64	elab 3638	. . . . . . . 8 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
66	48, 55, 65	3imtr4g 299	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
67		vex 3459	. . . . . . . . . 10 ⊢ ℎ ∈ V
68		f1oeq1 6808	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑓:𝐴–1-1-onto→𝐴 ↔ ℎ:𝐴–1-1-onto→𝐴))
69		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
70	69	neeq1d 3017	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) ≠ 𝑦 ↔ (ℎ‘𝑦) ≠ 𝑦))
71	70	ralbidv 3188	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
72	68, 71	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)))
73	67, 72	elab 3638	. . . . . . . . 9 ⊢ (ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
74	55, 73	anbi12i 639	. . . . . . . 8 ⊢ ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ↔ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)))
75	7	ad2antlr 739	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ^◡𝑠:𝐵–1-1-onto→𝐴)
76		f1ofo 6828	. . . . . . . . . . . 12 ⊢ (^◡𝑠:𝐵–1-1-onto→𝐴 → ^◡𝑠:𝐵–onto→𝐴)
77	75, 76	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ^◡𝑠:𝐵–onto→𝐴)
78	6	adantrr 729	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵)
79		f1ofn 6821	. . . . . . . . . . . 12 ⊢ ((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 → (𝑠 ∘ 𝑔) Fn 𝐴)
80	78, 79	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ 𝑔) Fn 𝐴)
81		simplr 780	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑠:𝐴–1-1-onto→𝐵)
82		simprrl 792	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴–1-1-onto→𝐴)
83		f1oco 6844	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐴–1-1-onto→𝐴) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵)
84	81, 82, 83	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵)
85		f1ofn 6821	. . . . . . . . . . . 12 ⊢ ((𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵 → (𝑠 ∘ ℎ) Fn 𝐴)
86	84, 85	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ) Fn 𝐴)
87		cocan2 7290	. . . . . . . . . . 11 ⊢ ((^◡𝑠:𝐵–onto→𝐴 ∧ (𝑠 ∘ 𝑔) Fn 𝐴 ∧ (𝑠 ∘ ℎ) Fn 𝐴) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
88	77, 80, 86, 87	syl3anc 1398	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
89		f1of1 6819	. . . . . . . . . . . 12 ⊢ (𝑠:𝐴–1-1-onto→𝐵 → 𝑠:𝐴–1-1→𝐵)
90	89	ad2antlr 739	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑠:𝐴–1-1→𝐵)
91		simprll 790	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴–1-1-onto→𝐴)
92		f1of 6820	. . . . . . . . . . . 12 ⊢ (𝑔:𝐴–1-1-onto→𝐴 → 𝑔:𝐴⟶𝐴)
93	91, 92	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴⟶𝐴)
94		f1of 6820	. . . . . . . . . . . 12 ⊢ (ℎ:𝐴–1-1-onto→𝐴 → ℎ:𝐴⟶𝐴)
95	82, 94	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴⟶𝐴)
96		cocan1 7289	. . . . . . . . . . 11 ⊢ ((𝑠:𝐴–1-1→𝐵 ∧ 𝑔:𝐴⟶𝐴 ∧ ℎ:𝐴⟶𝐴) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
97	90, 93, 95, 96	syl3anc 1398	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
98	88, 97	bitrd 282	. . . . . . . . 9 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ))
99	98	ex 417	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ)))
100	74, 99	biimtrid 245	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ)))
101	66, 100	dom2d 8986	. . . . . 6 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
102	101	ex 417	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})))
103	102	exlimdv 1963	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (∃𝑠 𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})))
104	2, 4, 103	mp2d 50	. . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})
105		enfii 9166	. . . . . 6 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
106	105	ancoms 463	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin)
107		deranglem 35658	. . . . 5 ⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
108	106, 107	syl 18	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
109		hashdom 14411	. . . 4 ⊢ (({𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin ∧ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) ↔ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
110	108, 4, 109	syl2anc 595	. . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) ↔ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
111	104, 110	mpbird 260	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
112		derang.d	. . . 4 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
113	112	derangval 35659	. . 3 ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
114	106, 113	syl 18	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
115	112	derangval 35659	. . 3 ⊢ (𝐵 ∈ Fin → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
116	115	adantl 486	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
117	111, 114, 116	3brtr4d 5143	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∃wex 1809 ∈ wcel 2143 {cab 2741 ≠ wne 2958 ∀wral 3079 class class class wbr 5109 ↦ cmpt 5192 ^◡ccnv 5660 ∘ ccom 5665 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 ≈ cen 8936 ≼ cdom 8937 Fincfn 8939 ≤ cle 11239 ♯chash 14362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12858 df-fz 13531 df-hash 14363

This theorem is referenced by: derangen 35664

W3C validator