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 35561

Description: One half of derangen 35562. (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 8952	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
2	1	birani 508	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → ∃𝑠 𝑠:𝐴–1-1-onto→𝐵)
3		deranglem 35556	. . . . 5 ⊢ (𝐵 ∈ Fin → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
4	3	adantl 486	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
5		f1oco 6845	. . . . . . . . . . . 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 6834	. . . . . . . . . . . 12 ⊢ (𝑠:𝐴–1-1-onto→𝐵 → ^◡𝑠:𝐵–1-1-onto→𝐴)
8	7	ad2antlr 739	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵–1-1-onto→𝐴)
9		f1oco 6845	. . . . . . . . . . 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 6268	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = (𝑠 ∘ (𝑔 ∘ ^◡𝑠))
12	11	fveq1i 6883	. . . . . . . . . . . . . 14 ⊢ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧)
13		simprl 782	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → 𝑔:𝐴–1-1-onto→𝐴)
14		f1oco 6845	. . . . . . . . . . . . . . . . 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 6821	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∘ ^◡𝑠):𝐵–1-1-onto→𝐴 → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
17	15, 16	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → (𝑔 ∘ ^◡𝑠):𝐵⟶𝐴)
18		fvco3 6982	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ ^◡𝑠):𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
19	17, 18	sylan 591	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠 ∘ (𝑔 ∘ ^◡𝑠))‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
20	12, 19	eqtrid 2816	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)))
21		f1of 6821	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑠:𝐵–1-1-onto→𝐴 → ^◡𝑠:𝐵⟶𝐴)
22	8, 21	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ^◡𝑠:𝐵⟶𝐴)
23		fvco3 6982	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
24	22, 23	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) = (𝑔‘(^◡𝑠‘𝑧)))
25	22	ffvelcdmda 7080	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (^◡𝑠‘𝑧) ∈ 𝐴)
26		simplrr 789	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)
27		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → (𝑔‘𝑦) = (𝑔‘(^◡𝑠‘𝑧)))
28		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝑠‘𝑧) → 𝑦 = (^◡𝑠‘𝑧))
29	27, 28	neeq12d 3025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (^◡𝑠‘𝑧) → ((𝑔‘𝑦) ≠ 𝑦 ↔ (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
30	29	rspcv 3586	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑠‘𝑧) ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦 → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧)))
31	25, 26, 30	sylc 66	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (𝑔‘(^◡𝑠‘𝑧)) ≠ (^◡𝑠‘𝑧))
32	24, 31	eqnetrd 3031	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ≠ (^◡𝑠‘𝑧))
33	32	necomd 3019	. . . . . . . . . . . . . 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 7080	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴)
36		f1ocnvfv 7277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠:𝐴–1-1-onto→𝐵 ∧ ((𝑔 ∘ ^◡𝑠)‘𝑧) ∈ 𝐴) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
37	34, 35, 36	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → ((𝑠‘((𝑔 ∘ ^◡𝑠)‘𝑧)) = 𝑧 → (^◡𝑠‘𝑧) = ((𝑔 ∘ ^◡𝑠)‘𝑧)))
38	37	necon3d 2985	. . . . . . . . . . . . . 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 3031	. . . . . . . . . . . 12 ⊢ (((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) ∧ 𝑧 ∈ 𝐵) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
41	40	ralrimiva 3163	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)) → ∀𝑧 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧)
42		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
43		id 23	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
44	42, 43	neeq12d 3025	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑧) ≠ 𝑧 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
45	44	cbvralvw 3249	. . . . . . . . . . 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 3467	. . . . . . . . 9 ⊢ 𝑔 ∈ V
50		f1oeq1 6809	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (𝑓:𝐴–1-1-onto→𝐴 ↔ 𝑔:𝐴–1-1-onto→𝐴))
51		fveq1 6881	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑦) = (𝑔‘𝑦))
52	51	neeq1d 3023	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑦) ≠ 𝑦 ↔ (𝑔‘𝑦) ≠ 𝑦))
53	52	ralbidv 3194	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
54	50, 53	anbi12d 643	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦)))
55	49, 54	elab 3647	. . . . . . . 8 ⊢ (𝑔 ∈ {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ↔ (𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦))
56		vex 3467	. . . . . . . . . . 11 ⊢ 𝑠 ∈ V
57	56, 49	coex 7926	. . . . . . . . . 10 ⊢ (𝑠 ∘ 𝑔) ∈ V
58	56	cnvex 7921	. . . . . . . . . 10 ⊢ ^◡𝑠 ∈ V
59	57, 58	coex 7926	. . . . . . . . 9 ⊢ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) ∈ V
60		f1oeq1 6809	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓:𝐵–1-1-onto→𝐵 ↔ ((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵))
61		fveq1 6881	. . . . . . . . . . . 12 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (𝑓‘𝑦) = (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦))
62	61	neeq1d 3023	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓‘𝑦) ≠ 𝑦 ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
63	62	ralbidv 3194	. . . . . . . . . 10 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → (∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦))
64	60, 63	anbi12d 643	. . . . . . . . 9 ⊢ (𝑓 = ((𝑠 ∘ 𝑔) ∘ ^◡𝑠) → ((𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦) ↔ (((𝑠 ∘ 𝑔) ∘ ^◡𝑠):𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (((𝑠 ∘ 𝑔) ∘ ^◡𝑠)‘𝑦) ≠ 𝑦)))
65	59, 64	elab 3647	. . . . . . . 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 3467	. . . . . . . . . 10 ⊢ ℎ ∈ V
68		f1oeq1 6809	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑓:𝐴–1-1-onto→𝐴 ↔ ℎ:𝐴–1-1-onto→𝐴))
69		fveq1 6881	. . . . . . . . . . . . 13 ⊢ (𝑓 = ℎ → (𝑓‘𝑦) = (ℎ‘𝑦))
70	69	neeq1d 3023	. . . . . . . . . . . 12 ⊢ (𝑓 = ℎ → ((𝑓‘𝑦) ≠ 𝑦 ↔ (ℎ‘𝑦) ≠ 𝑦))
71	70	ralbidv 3194	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))
72	68, 71	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦) ↔ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦)))
73	67, 72	elab 3647	. . . . . . . . 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 6829	. . . . . . . . . . . 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 6822	. . . . . . . . . . . 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 6845	. . . . . . . . . . . . 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 6822	. . . . . . . . . . . 12 ⊢ ((𝑠 ∘ ℎ):𝐴–1-1-onto→𝐵 → (𝑠 ∘ ℎ) Fn 𝐴)
86	84, 85	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (𝑠 ∘ ℎ) Fn 𝐴)
87		cocan2 7291	. . . . . . . . . . 11 ⊢ ((^◡𝑠:𝐵–onto→𝐴 ∧ (𝑠 ∘ 𝑔) Fn 𝐴 ∧ (𝑠 ∘ ℎ) Fn 𝐴) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
88	77, 80, 86, 87	syl3anc 1396	. . . . . . . . . 10 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → (((𝑠 ∘ 𝑔) ∘ ^◡𝑠) = ((𝑠 ∘ ℎ) ∘ ^◡𝑠) ↔ (𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ)))
89		f1of1 6820	. . . . . . . . . . . 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 6821	. . . . . . . . . . . 12 ⊢ (𝑔:𝐴–1-1-onto→𝐴 → 𝑔:𝐴⟶𝐴)
93	91, 92	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → 𝑔:𝐴⟶𝐴)
94		f1of 6821	. . . . . . . . . . . 12 ⊢ (ℎ:𝐴–1-1-onto→𝐴 → ℎ:𝐴⟶𝐴)
95	82, 94	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝑠:𝐴–1-1-onto→𝐵) ∧ ((𝑔:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ≠ 𝑦) ∧ (ℎ:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ≠ 𝑦))) → ℎ:𝐴⟶𝐴)
96		cocan1 7290	. . . . . . . . . . 11 ⊢ ((𝑠:𝐴–1-1→𝐵 ∧ 𝑔:𝐴⟶𝐴 ∧ ℎ:𝐴⟶𝐴) → ((𝑠 ∘ 𝑔) = (𝑠 ∘ ℎ) ↔ 𝑔 = ℎ))
97	90, 93, 95, 96	syl3anc 1396	. . . . . . . . . 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 8989	. . . . . 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 1960	. . . 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 9169	. . . . . 6 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
106	105	ancoms 463	. . . . 5 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin)
107		deranglem 35556	. . . . 5 ⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
108	106, 107	syl 18	. . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)} ∈ Fin)
109		hashdom 14414	. . . 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 35557	. . 3 ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
114	106, 113	syl 18	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
115	112	derangval 35557	. . 3 ⊢ (𝐵 ∈ Fin → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
116	115	adantl 486	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐵) = (♯‘{𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝑓‘𝑦) ≠ 𝑦)}))
117	111, 114, 116	3brtr4d 5147	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∃wex 1806 ∈ wcel 2149 {cab 2747 ≠ wne 2964 ∀wral 3085 class class class wbr 5113 ↦ cmpt 5196 ^◡ccnv 5661 ∘ ccom 5666 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 ≈ cen 8939 ≼ cdom 8940 Fincfn 8942 ≤ cle 11243 ♯chash 14365

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-fz 13535 df-hash 14366

This theorem is referenced by: derangen 35562

W3C validator