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	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to A ≼ B$

Proof

Step	Hyp	Ref	Expression
1		f1cnv	$⊢ F : A \underset{1-1}{⟶} B \to F^{-1} : ran F \underset{1-1 onto}{⟶} A$
2		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
3	2	frnd	$⊢ F : A \underset{1-1}{⟶} B \to ran F \subseteq B$
4		ssfi	$⊢ (B \in Fin \land ran F \subseteq B) \to ran F \in Fin$
5	3 4	sylan2	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to ran F \in Fin$
6		f1ofn	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} A \to F^{-1} Fn ran F$
7		fnfi	$⊢ (F^{-1} Fn ran F \land ran F \in Fin) \to F^{-1} \in Fin$
8	6 7	sylan	$⊢ (F^{-1} : ran F \underset{1-1 onto}{⟶} A \land ran F \in Fin) \to F^{-1} \in Fin$
9	1 5 8	syl2an2	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to F^{-1} \in Fin$
10		cnvfi	$⊢ F^{-1} \in Fin \to {F^{-1}}^{-1} \in Fin$
11		f1rel	$⊢ F : A \underset{1-1}{⟶} B \to Rel F$
12		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
13	11 12	sylib	$⊢ F : A \underset{1-1}{⟶} B \to {F^{-1}}^{-1} = F$
14	13	eleq1d	$⊢ F : A \underset{1-1}{⟶} B \to ({F^{-1}}^{-1} \in Fin \leftrightarrow F \in Fin)$
15	14	biimpac	$⊢ ({F^{-1}}^{-1} \in Fin \land F : A \underset{1-1}{⟶} B) \to F \in Fin$
16	10 15	sylan	$⊢ (F^{-1} \in Fin \land F : A \underset{1-1}{⟶} B) \to F \in Fin$
17	9 16	sylancom	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to F \in Fin$
18		f1dom3g	$⊢ (F \in Fin \land B \in Fin \land F : A \underset{1-1}{⟶} B) \to A ≼ B$
19	18	3expib	$⊢ F \in Fin \to ((B \in Fin \land F : A \underset{1-1}{⟶} B) \to A ≼ B)$
20	17 19	mpcom	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to A ≼ B$

Metamath Proof Explorer

Theorem f1domfi

Proof