Step |
Hyp |
Ref |
Expression |
1 |
|
f1f |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
2 |
1
|
frnd |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ran 𝐹 ⊆ 𝐵 ) |
3 |
|
ssfi |
⊢ ( ( 𝐵 ∈ Fin ∧ ran 𝐹 ⊆ 𝐵 ) → ran 𝐹 ∈ Fin ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ran 𝐹 ∈ Fin ) |
5 |
|
f1f1orn |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) |
6 |
5
|
adantl |
⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) |
7 |
|
f1ocnv |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 ) |
8 |
|
f1ofo |
⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 → ◡ 𝐹 : ran 𝐹 –onto→ 𝐴 ) |
9 |
6 7 8
|
3syl |
⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ◡ 𝐹 : ran 𝐹 –onto→ 𝐴 ) |
10 |
|
fofi |
⊢ ( ( ran 𝐹 ∈ Fin ∧ ◡ 𝐹 : ran 𝐹 –onto→ 𝐴 ) → 𝐴 ∈ Fin ) |
11 |
4 9 10
|
syl2anc |
⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ∈ Fin ) |