Metamath Proof Explorer

Theorem 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 ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 )
2 1 frnd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ran 𝐹 ⊆ dom 𝐸 )
3 2 adantl ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ran 𝐹 ⊆ dom 𝐸 )
4 ssdmres ⊢ ( ran 𝐹 ⊆ dom 𝐸 ↔ dom ( 𝐸 ↾ ran 𝐹 ) = ran 𝐹 )
5 3 4 sylib ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → dom ( 𝐸 ↾ ran 𝐹 ) = ran 𝐹 )
6 5 fveq2d ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ dom ( 𝐸 ↾ ran 𝐹 ) ) = ( ♯ ‘ ran 𝐹 ) )
7 df-ima ⊢ ( 𝐸 “ ran 𝐹 ) = ran ( 𝐸 ↾ ran 𝐹 )
8 7 fveq2i ⊢ ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ ran ( 𝐸 ↾ ran 𝐹 ) )
9 f1fun ⊢ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 → Fun 𝐸 )
10 funres ⊢ ( Fun 𝐸 → Fun ( 𝐸 ↾ ran 𝐹 ) )
11 10 funfnd ⊢ ( Fun 𝐸 → ( 𝐸 ↾ ran 𝐹 ) Fn dom ( 𝐸 ↾ ran 𝐹 ) )
12 9 11 syl ⊢ ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 → ( 𝐸 ↾ ran 𝐹 ) Fn dom ( 𝐸 ↾ ran 𝐹 ) )
13 12 ad2antrr ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( 𝐸 ↾ ran 𝐹 ) Fn dom ( 𝐸 ↾ ran 𝐹 ) )
14 hashfn ⊢ ( ( 𝐸 ↾ ran 𝐹 ) Fn dom ( 𝐸 ↾ ran 𝐹 ) → ( ♯ ‘ ( 𝐸 ↾ ran 𝐹 ) ) = ( ♯ ‘ dom ( 𝐸 ↾ ran 𝐹 ) ) )
15 13 14 syl ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ↾ ran 𝐹 ) ) = ( ♯ ‘ dom ( 𝐸 ↾ ran 𝐹 ) ) )
16 ovex ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V
17 fex ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐸 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V ) → 𝐹 ∈ V )
18 1 16 17 sylancl ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → 𝐹 ∈ V )
19 rnexg ⊢ ( 𝐹 ∈ V → ran 𝐹 ∈ V )
20 18 19 syl ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ran 𝐹 ∈ V )
21 simpll ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → 𝐸 : dom 𝐸 –1-1→ ran 𝐸 )
22 f1ssres ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ ran 𝐹 ⊆ dom 𝐸 ) → ( 𝐸 ↾ ran 𝐹 ) : ran 𝐹 –1-1→ ran 𝐸 )
23 21 3 22 syl2anc ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( 𝐸 ↾ ran 𝐹 ) : ran 𝐹 –1-1→ ran 𝐸 )
24 hashf1rn ⊢ ( ( ran 𝐹 ∈ V ∧ ( 𝐸 ↾ ran 𝐹 ) : ran 𝐹 –1-1→ ran 𝐸 ) → ( ♯ ‘ ( 𝐸 ↾ ran 𝐹 ) ) = ( ♯ ‘ ran ( 𝐸 ↾ ran 𝐹 ) ) )
25 20 23 24 syl2an2 ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ↾ ran 𝐹 ) ) = ( ♯ ‘ ran ( 𝐸 ↾ ran 𝐹 ) ) )
26 15 25 eqtr3d ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ dom ( 𝐸 ↾ ran 𝐹 ) ) = ( ♯ ‘ ran ( 𝐸 ↾ ran 𝐹 ) ) )
27 8 26 eqtr4id ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ dom ( 𝐸 ↾ ran 𝐹 ) ) )
28 hashf1rn ⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )
29 16 28 mpan ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )
30 29 adantl ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )
31 6 27 30 3eqtr4d ⊢ ( ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ 𝐹 ) )
32 31 ex ⊢ ( ( 𝐸 : dom 𝐸 –1-1→ ran 𝐸 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐸 → ( ♯ ‘ ( 𝐸 “ ran 𝐹 ) ) = ( ♯ ‘ 𝐹 ) ) )