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 35176

Description: One half of derangen 35177. (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		simpl 482	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ≈ 𝐵)
2		bren 8995	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
3	1, 2	sylib 218	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
4		deranglem 35171	. . . . 5 ⊢ (𝐵 ∈ Fin → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
5	4	adantl 481	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
6		f1oco 6871	. . . . . . . . . . . 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 6860	. . . . . . . . . . . 12 ⊢ (𝑠:𝐴–1-1-onto→𝐵 → ^◡𝑠:𝐵–1-1-onto→𝐴)
9	8	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵–1-1-onto→𝐴)
10		f1oco 6871	. . . . . . . . . . 11 ⊢ (((𝑠 ∘ 𝑔):𝐴–1-1-onto→𝐵 ∧ ^◡𝑠:𝐵–1-1-onto→𝐴) → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵)
11	7, 9, 10	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵)
12		coass 6285	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = (𝑠 ∘ (𝑔 ∘ ^◡𝑠))
13	12	fveq1i 6907	. . . . . . . . . . . . . 14 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧)
14		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → 𝑔:𝐴–1-1-onto→𝐴)
15		f1oco 6871	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ^◡𝑠:𝐵–1-1-onto→𝐴) → (𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴)
16	14, 9, 15	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴)
17		f1of 6848	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴 → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
18	16, 17	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
19		fvco3 7008	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ ^◡𝑠):𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
20	18, 19	sylan 580	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
21	13, 20	eqtrid 2789	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
22		f1of 6848	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑠:𝐵–1-1-onto→𝐴 → ^◡𝑠:𝐵⟶𝐴)
23	9, 22	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵⟶𝐴)
24		fvco3 7008	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
25	23, 24	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
26	23	ffvelcdmda 7104	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ∈ 𝐴)
27		simplrr 778	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)
28		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → (𝑔‘𝑦) = (𝑔‘(^◡𝑠‘𝑧)))
29		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → 𝑦 = (^◡𝑠‘𝑧))
30	28, 29	neeq12d 3002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (^◡𝑠‘𝑧) → ((𝑔‘𝑦) ≠ 𝑦 ↔ (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
31	30	rspcv 3618	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠‘𝑧) ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦 → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
32	26, 27, 31	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧))
33	25, 32	eqnetrd 3008	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ≠ (^◡𝑠‘𝑧))
34	33	necomd 2996	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ≠ ((𝑔 ∘ ^◡𝑠)‘𝑧))
35		simpllr 776	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → 𝑠:𝐴–1-1-onto→𝐵)
36	18	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴)
37		f1ocnvfv 7298	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
38	35, 36, 37	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
39	38	necon3d 2961	. . . . . . . . . . . . . 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 3008	. . . . . . . . . . . 12 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
42	41	ralrimiva 3146	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
43		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
44		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
45	43, 44	neeq12d 3002	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
46	45	cbvralvw 3237	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)
47	42, 46	sylib 218	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)
48	11, 47	jca 511	. . . . . . . . 9 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
49	48	ex 412	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
50		vex 3484	. . . . . . . . 9 ⊢ 𝑔 ∈ V
51		f1oeq1 6836	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓:𝐴–1-1-onto→𝐴 ↔ 𝑔:𝐴–1-1-onto→𝐴))
52		fveq1 6905	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑦) = (𝑔‘𝑦))
53	52	neeq1d 3000	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑔‘𝑦) ≠ 𝑦))
54	53	ralbidv 3178	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
55	51, 54	anbi12d 632	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)))
56	50, 55	elab 3679	. . . . . . . 8 ⊢ (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
57		vex 3484	. . . . . . . . . . 11 ⊢ 𝑠 ∈ V
58	57, 50	coex 7952	. . . . . . . . . 10 ⊢ (𝑠 ∘ 𝑔) ∈ V
59	57	cnvex 7947	. . . . . . . . . 10 ⊢ ^◡𝑠 ∈ V
60	58, 59	coex 7952	. . . . . . . . 9 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ V
61		f1oeq1 6836	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓:𝐵–1-1-onto→𝐵 ↔ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵))
62		fveq1 6905	. . . . . . . . . . . 12 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓‘𝑦) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
63	62	neeq1d 3000	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
64	63	ralbidv 3178	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
65	61, 64	anbi12d 632	. . . . . . . . 9 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦) ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
66	60, 65	elab 3679	. . . . . . . 8 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
67	49, 56, 66	3imtr4g 296	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} → ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
68		vex 3484	. . . . . . . . . 10 ⊢ ℎ ∈ V
69		f1oeq1 6836	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑓:𝐴–1-1-onto→𝐴 ↔ ℎ:𝐴–1-1-onto→𝐴))
70		fveq1 6905	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
71	70	neeq1d 3000	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) ≠ 𝑦 ↔ (ℎ‘𝑦) ≠ 𝑦))
72	71	ralbidv 3178	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
73	69, 72	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)))
74	68, 73	elab 3679	. . . . . . . . 9 ⊢ (ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
75	56, 74	anbi12i 628	. . . . . . . 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 6855	. . . . . . . . . . . 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 6849	. . . . . . . . . . . 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 6871	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ℎ:𝐴–1-1-onto→𝐴) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵)
85	82, 83, 84	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵)
86		f1ofn 6849	. . . . . . . . . . . 12 ⊢ ((𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵 → (𝑠 ∘ ℎ) Fn 𝐴)
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ) Fn 𝐴)
88		cocan2 7312	. . . . . . . . . . 11 ⊢ ((^◡𝑠:𝐵–onto→𝐴 ∧ (𝑠 ∘ 𝑔) Fn 𝐴 ∧ (𝑠 ∘ ℎ) Fn 𝐴) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
89	78, 81, 87, 88	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
90		f1of1 6847	. . . . . . . . . . . 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 6848	. . . . . . . . . . . 12 ⊢ (𝑔:𝐴–1-1-onto→𝐴 → 𝑔:𝐴⟶𝐴)
94	92, 93	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴⟶𝐴)
95		f1of 6848	. . . . . . . . . . . 12 ⊢ (ℎ:𝐴–1-1-onto→𝐴 → ℎ:𝐴⟶𝐴)
96	83, 95	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴⟶𝐴)
97		cocan1 7311	. . . . . . . . . . 11 ⊢ ((𝑠:𝐴–1-1→𝐵 ∧ 𝑔:𝐴⟶𝐴 ∧ ℎ:𝐴⟶𝐴) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
98	91, 94, 96, 97	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
99	89, 98	bitrd 279	. . . . . . . . 9 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ))
100	99	ex 412	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → (((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ)))
101	75, 100	biimtrid 242	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ((𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∧ ℎ ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ 𝑔 = ℎ)))
102	67, 101	dom2d 9033	. . . . . 6 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
103	102	ex 412	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝑠:𝐴–1-1-onto→𝐵 → ({𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)})))
104	103	exlimdv 1933	. . . 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 9226	. . . . . 6 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
107	106	ancoms 458	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin)
108		deranglem 35171	. . . . 5 ⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
109	107, 108	syl 17	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
110		hashdom 14418	. . . 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 584	. . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}) ↔ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
112	105, 111	mpbird 257	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
113		derang.d	. . . 4 ⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))
114	113	derangval 35172	. . 3 ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
115	107, 114	syl 17	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
116	113	derangval 35172	. . 3 ⊢ (𝐵 ∈ Fin → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
117	116	adantl 481	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
118	112, 115, 117	3brtr4d 5175	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 {cab 2714 ≠ wne 2940 ∀wral 3061 class class class wbr 5143 ↦ cmpt 5225 ^◡ccnv 5684 ∘ ccom 5689 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 ≈ cen 8982 ≼ cdom 8983 Fincfn 8985 ≤ cle 11296 ♯chash 14369

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-oadd 8510 df-er 8745 df-map 8868 df-pm 8869 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-fz 13548 df-hash 14370

This theorem is referenced by: derangen 35177

W3C validator