Theorem f1domfi

Description: If the codomain of a one-to-one function is finite, then the function's domain is dominated by its codomain. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1domg ). (Contributed by BTernaryTau, 25-Sep-2024)

	Ref	Expression
Assertion	f1domfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1cnv	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 )
2		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
3	2	frnd	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ran 𝐹 ⊆ 𝐵 )
4		ssfi	⊢ ( ( 𝐵 ∈ Fin ∧ ran 𝐹 ⊆ 𝐵 ) → ran 𝐹 ∈ Fin )
5	3 4	sylan2	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ran 𝐹 ∈ Fin )
6		f1ofn	⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 → ◡ 𝐹 Fn ran 𝐹 )
7		fnfi	⊢ ( ( ◡ 𝐹 Fn ran 𝐹 ∧ ran 𝐹 ∈ Fin ) → ◡ 𝐹 ∈ Fin )
8	6 7	sylan	⊢ ( ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 ∧ ran 𝐹 ∈ Fin ) → ◡ 𝐹 ∈ Fin )
9	1 5 8	syl2an2	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ◡ 𝐹 ∈ Fin )
10		cnvfi	⊢ ( ◡ 𝐹 ∈ Fin → ◡ ◡ 𝐹 ∈ Fin )
11		f1rel	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Rel 𝐹 )
12		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
13	11 12	sylib	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ◡ ◡ 𝐹 = 𝐹 )
14	13	eleq1d	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ◡ ◡ 𝐹 ∈ Fin ↔ 𝐹 ∈ Fin ) )
15	14	biimpac	⊢ ( ( ◡ ◡ 𝐹 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ Fin )
16	10 15	sylan	⊢ ( ( ◡ 𝐹 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ Fin )
17	9 16	sylancom	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ Fin )
18		f1dom3g	⊢ ( ( 𝐹 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 )
19	18	3expib	⊢ ( 𝐹 ∈ Fin → ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) )
20	17 19	mpcom	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 )