This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 ) → 𝐴 ≼ 𝐵 )