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 35399

Description: One half of derangen 35400. (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 8893	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
2	1	birani 504	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
3		deranglem 35394	. . . . 5 ⊢ (𝐵 ∈ Fin → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	3	adantl 482	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
5		f1oco 6790	. . . . . . . . . . . 12 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ 𝑔:𝐴–1-1-onto→𝐴) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵)
6	5	ad2ant2lr 754	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵)
7		f1ocnv 6779	. . . . . . . . . . . 12 ⊢ (𝑠:𝐴–1-1-onto→𝐵 → ^◡𝑠:𝐵–1-1-onto→𝐴)
8	7	ad2antlr 733	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵–1-1-onto→𝐴)
9		f1oco 6790	. . . . . . . . . . 11 ⊢ (((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 ∧ ^◡𝑠:𝐵–1-1-onto→𝐴) → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵)
10	6, 8, 9	syl2anc 590	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵)
11		coass 6217	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = (𝑠 ∘ (𝑔 ∘ ^◡𝑠))
12	11	fveq1i 6828	. . . . . . . . . . . . . 14 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧)
13		simprl 776	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → 𝑔:𝐴–1-1-onto→𝐴)
14		f1oco 6790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ^◡𝑠:𝐵–1-1-onto→𝐴) → (𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴)
15	13, 8, 14	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴)
16		f1of 6767	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴 → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
17	15, 16	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
18		fvco3 6927	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ ^◡𝑠):𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
19	17, 18	sylan 586	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
20	12, 19	eqtrid 2786	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
21		f1of 6767	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑠:𝐵–1-1-onto→𝐴 → ^◡𝑠:𝐵⟶𝐴)
22	8, 21	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵⟶𝐴)
23		fvco3 6927	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
24	22, 23	sylan 586	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
25	22	ffvelcdmda 7025	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ∈ 𝐴)
26		simplrr 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)
27		fveq2 6827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → (𝑔‘𝑦) = (𝑔‘(^◡𝑠‘𝑧)))
28		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → 𝑦 = (^◡𝑠‘𝑧))
29	27, 28	neeq12d 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (^◡𝑠‘𝑧) → ((𝑔‘𝑦) ≠ 𝑦 ↔ (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
30	29	rspcv 3556	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠‘𝑧) ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦 → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
31	25, 26, 30	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧))
32	24, 31	eqnetrd 3001	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ≠ (^◡𝑠‘𝑧))
33	32	necomd 2989	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ≠ ((𝑔 ∘ ^◡𝑠)‘𝑧))
34		simpllr 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → 𝑠:𝐴–1-1-onto→𝐵)
35	17	ffvelcdmda 7025	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴)
36		f1ocnvfv 7222	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
37	34, 35, 36	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
38	37	necon3d 2955	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((^◡𝑠‘𝑧) ≠ ((𝑔 ∘ ^◡𝑠)‘𝑧) → (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) ≠ 𝑧))
39	33, 38	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) ≠ 𝑧)
40	20, 39	eqnetrd 3001	. . . . . . . . . . . 12 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
41	40	ralrimiva 3131	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
42		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
43		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
44	42, 43	neeq12d 2995	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
45	44	cbvralvw 3217	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)
46	41, 45	sylib 219	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)
47	10, 46	jca 516	. . . . . . . . 9 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
48	47	ex 413	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
49		vex 3435	. . . . . . . . 9 ⊢ 𝑔 ∈ V
50		f1oeq1 6755	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓:𝐴–1-1-onto→𝐴 ↔ 𝑔:𝐴–1-1-onto→𝐴))
51		fveq1 6826	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑦) = (𝑔‘𝑦))
52	51	neeq1d 2993	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑔‘𝑦) ≠ 𝑦))
53	52	ralbidv 3162	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
54	50, 53	anbi12d 638	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)))
55	49, 54	elab 3617	. . . . . . . 8 ⊢ (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
56		vex 3435	. . . . . . . . . . 11 ⊢ 𝑠 ∈ V
57	56, 49	coex 7870	. . . . . . . . . 10 ⊢ (𝑠 ∘ 𝑔) ∈ V
58	56	cnvex 7865	. . . . . . . . . 10 ⊢ ^◡𝑠 ∈ V
59	57, 58	coex 7870	. . . . . . . . 9 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ V
60		f1oeq1 6755	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓:𝐵–1-1-onto→𝐵 ↔ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵))
61		fveq1 6826	. . . . . . . . . . . 12 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓‘𝑦) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
62	61	neeq1d 2993	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
63	62	ralbidv 3162	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
64	60, 63	anbi12d 638	. . . . . . . . 9 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦) ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
65	59, 64	elab 3617	. . . . . . . 8 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
66	48, 55, 65	3imtr4g 297	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
67		vex 3435	. . . . . . . . . 10 ⊢ ℎ ∈ V
68		f1oeq1 6755	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑓:𝐴–1-1-onto→𝐴 ↔ ℎ:𝐴–1-1-onto→𝐴))
69		fveq1 6826	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
70	69	neeq1d 2993	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) ≠ 𝑦 ↔ (ℎ‘𝑦) ≠ 𝑦))
71	70	ralbidv 3162	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
72	68, 71	anbi12d 638	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)))
73	67, 72	elab 3617	. . . . . . . . 9 ⊢ (ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
74	55, 73	anbi12i 634	. . . . . . . 8 ⊢ ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ↔ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)))
75	7	ad2antlr 733	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ^◡𝑠:𝐵–1-1-onto→𝐴)
76		f1ofo 6774	. . . . . . . . . . . 12 ⊢ (^◡𝑠:𝐵–1-1-onto→𝐴 → ^◡𝑠:𝐵–onto→𝐴)
77	75, 76	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ^◡𝑠:𝐵–onto→𝐴)
78	6	adantrr 723	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵)
79		f1ofn 6768	. . . . . . . . . . . 12 ⊢ ((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 → (𝑠 ∘ 𝑔) Fn 𝐴)
80	78, 79	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ 𝑔) Fn 𝐴)
81		simplr 774	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑠:𝐴–1-1-onto→𝐵)
82		simprrl 786	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴–1-1-onto→𝐴)
83		f1oco 6790	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐴–1-1-onto→𝐴) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵)
84	81, 82, 83	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵)
85		f1ofn 6768	. . . . . . . . . . . 12 ⊢ ((𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵 → (𝑠 ∘ ℎ) Fn 𝐴)
86	84, 85	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ) Fn 𝐴)
87		cocan2 7236	. . . . . . . . . . 11 ⊢ ((^◡𝑠:𝐵–onto→𝐴 ∧ (𝑠 ∘ 𝑔) Fn 𝐴 ∧ (𝑠 ∘ ℎ) Fn 𝐴) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
88	77, 80, 86, 87	syl3anc 1379	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
89		f1of1 6766	. . . . . . . . . . . 12 ⊢ (𝑠:𝐴–1-1-onto→𝐵 → 𝑠:𝐴–1-1→𝐵)
90	89	ad2antlr 733	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑠:𝐴–1-1→𝐵)
91		simprll 784	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴–1-1-onto→𝐴)
92		f1of 6767	. . . . . . . . . . . 12 ⊢ (𝑔:𝐴–1-1-onto→𝐴 → 𝑔:𝐴⟶𝐴)
93	91, 92	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴⟶𝐴)
94		f1of 6767	. . . . . . . . . . . 12 ⊢ (ℎ:𝐴–1-1-onto→𝐴 → ℎ:𝐴⟶𝐴)
95	82, 94	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴⟶𝐴)
96		cocan1 7235	. . . . . . . . . . 11 ⊢ ((𝑠:𝐴–1-1→𝐵 ∧ 𝑔:𝐴⟶𝐴 ∧ ℎ:𝐴⟶𝐴) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
97	90, 93, 95, 96	syl3anc 1379	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
98	88, 97	bitrd 280	. . . . . . . . 9 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ))
99	98	ex 413	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ)))
100	74, 99	biimtrid 243	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ)))
101	66, 100	dom2d 8930	. . . . . 6 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
102	101	ex 413	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})))
103	102	exlimdv 1940	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (∃𝑠 𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})))
104	2, 4, 103	mp2d 49	. . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})
105		enfii 9110	. . . . . 6 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
106	105	ancoms 459	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin)
107		deranglem 35394	. . . . 5 ⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
108	106, 107	syl 17	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
109		hashdom 14332	. . . 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 590	. . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) ↔ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
111	104, 110	mpbird 258	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
112		derang.d	. . . 4 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
113	112	derangval 35395	. . 3 ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
114	106, 113	syl 17	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
115	112	derangval 35395	. . 3 ⊢ (𝐵 ∈ Fin → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
116	115	adantl 482	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
117	111, 114, 116	3brtr4d 5104	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∃wex 1786 ∈ wcel 2119 {cab 2717 ≠ wne 2934 ∀wral 3053 class class class wbr 5072 ↦ cmpt 5153 ^◡ccnv 5617 ∘ ccom 5622 Fn wfn 6480 ⟶wf 6481 –1-1→wf1 6482 –onto→wfo 6483 –1-1-onto→wf1o 6484 ‘cfv 6485 ≈ cen 8880 ≼ cdom 8881 Fincfn 8883 ≤ cle 11171 ♯chash 14283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-oadd 8399 df-er 8633 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-fz 13453 df-hash 14284

This theorem is referenced by: derangen 35400

W3C validator