Description: If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike f1dom2g ). (Contributed by BTernaryTau, 24-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | f1domfi2 | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1fn | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 ) | |
| 2 | fnfi | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐹 ∈ Fin ) | |
| 3 | 1 2 | sylan | ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ Fin ) → 𝐹 ∈ Fin ) |
| 4 | 3 | ancoms | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ Fin ) |
| 5 | 4 | 3adant2 | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ Fin ) |
| 6 | f1dom3g | ⊢ ( ( 𝐹 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) | |
| 7 | 5 6 | syld3an1 | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ 𝐵 ) |