Metamath Proof Explorer

Theorem hashf1rn

Description: The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 4-May-2021)

Ref Expression
Assertion hashf1rn ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 1 anim2i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) )
3 2 ancomd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) )
4 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
5 3 4 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ V )
6 f1o2ndf1 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 )
7 df-2nd ⊢ 2nd = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )
8 7 funmpt2 ⊢ Fun 2nd
9 resfunexg ⊢ ( ( Fun 2nd ∧ 𝐹 ∈ V ) → ( 2nd ↾ 𝐹 ) ∈ V )
10 8 5 9 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 2nd ↾ 𝐹 ) ∈ V )
11 f1oeq1 ⊢ ( ( 2nd ↾ 𝐹 ) = 𝑓 → ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 ↔ 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) )
12 11 biimpd ⊢ ( ( 2nd ↾ 𝐹 ) = 𝑓 → ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 → 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) )
13 12 eqcoms ⊢ ( 𝑓 = ( 2nd ↾ 𝐹 ) → ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 → 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) )
14 13 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑓 = ( 2nd ↾ 𝐹 ) ) → ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 → 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) )
15 10 14 spcimedv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 → ∃ 𝑓 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) )
16 15 ex ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 → ∃ 𝑓 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) ) )
17 16 com13 ⊢ ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐴 ∈ 𝑉 → ∃ 𝑓 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) ) )
18 6 17 mpcom ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐴 ∈ 𝑉 → ∃ 𝑓 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 ) )
19 18 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 )
20 hasheqf1oi ⊢ ( 𝐹 ∈ V → ( ∃ 𝑓 𝑓 : 𝐹 –1-1-onto→ ran 𝐹 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) ) )
21 5 19 20 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ran 𝐹 ) )