hashimarn

Description: The size of the image of a one-to-one function E under the range of a function F which is a one-to-one function into the domain of E equals the size of the function F . (Contributed by Alexander van der Vekens, 4-Feb-2018) (Proof shortened by AV, 4-May-2021)

		Ref	Expression
	Assertion	hashimarn	$⊢ (E : dom E \underset{1-1}{⟶} ran E \land E \in V) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to \|E [ran F]\| = \|F\|)$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to F : (0 ..^\|F\|) ⟶ dom E$
2	1	frnd	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to ran F \subseteq dom E$
3	2	adantl	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to ran F \subseteq dom E$
4		ssdmres	$⊢ ran F \subseteq dom E \leftrightarrow dom ({E ↾}_{ran F}) = ran F$
5	3 4	sylib	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to dom ({E ↾}_{ran F}) = ran F$
6	5	fveq2d	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|dom ({E ↾}_{ran F})\| = \|ran F\|$
7		df-ima	$⊢ E [ran F] = ran ({E ↾}_{ran F})$
8	7	fveq2i	$⊢ \|E [ran F]\| = \|ran ({E ↾}_{ran F})\|$
9		f1fun	$⊢ E : dom E \underset{1-1}{⟶} ran E \to Fun E$
10		funres	$⊢ Fun E \to Fun ({E ↾}_{ran F})$
11	10	funfnd	$⊢ Fun E \to ({E ↾}_{ran F}) Fn dom ({E ↾}_{ran F})$
12	9 11	syl	$⊢ E : dom E \underset{1-1}{⟶} ran E \to ({E ↾}_{ran F}) Fn dom ({E ↾}_{ran F})$
13	12	ad2antrr	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to ({E ↾}_{ran F}) Fn dom ({E ↾}_{ran F})$
14		hashfn	$⊢ ({E ↾}_{ran F}) Fn dom ({E ↾}_{ran F}) \to \|{E ↾}_{ran F}\| = \|dom ({E ↾}_{ran F})\|$
15	13 14	syl	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|{E ↾}_{ran F}\| = \|dom ({E ↾}_{ran F})\|$
16		ovex	$⊢ (0 ..^\|F\|) \in V$
17		fex	$⊢ (F : (0 ..^\|F\|) ⟶ dom E \land (0 ..^\|F\|) \in V) \to F \in V$
18	1 16 17	sylancl	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to F \in V$
19		rnexg	$⊢ F \in V \to ran F \in V$
20	18 19	syl	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to ran F \in V$
21		simpll	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to E : dom E \underset{1-1}{⟶} ran E$
22		f1ssres	$⊢ (E : dom E \underset{1-1}{⟶} ran E \land ran F \subseteq dom E) \to ({E ↾}_{ran F}) : ran F \underset{1-1}{⟶} ran E$
23	21 3 22	syl2anc	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to ({E ↾}_{ran F}) : ran F \underset{1-1}{⟶} ran E$
24		hashf1rn	$⊢ (ran F \in V \land ({E ↾}_{ran F}) : ran F \underset{1-1}{⟶} ran E) \to \|{E ↾}_{ran F}\| = \|ran ({E ↾}_{ran F})\|$
25	20 23 24	syl2an2	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|{E ↾}_{ran F}\| = \|ran ({E ↾}_{ran F})\|$
26	15 25	eqtr3d	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|dom ({E ↾}_{ran F})\| = \|ran ({E ↾}_{ran F})\|$
27	8 26	eqtr4id	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|E [ran F]\| = \|dom ({E ↾}_{ran F})\|$
28		hashf1rn	$⊢ ((0 ..^\|F\|) \in V \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|F\| = \|ran F\|$
29	16 28	mpan	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to \|F\| = \|ran F\|$
30	29	adantl	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|F\| = \|ran F\|$
31	6 27 30	3eqtr4d	$⊢ ((E : dom E \underset{1-1}{⟶} ran E \land E \in V) \land F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E) \to \|E [ran F]\| = \|F\|$
32	31	ex	$⊢ (E : dom E \underset{1-1}{⟶} ran E \land E \in V) \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \to \|E [ran F]\| = \|F\|)$

Metamath Proof Explorer

Theorem hashimarn

Proof