Theorem f1imaenfi 8914

Description: If a function is one-to-one, then the image of a finite subset of its domain under it is equinumerous to the subset. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1imaeng 8732). (Contributed by BTernaryTau, 29-Sep-2024.)

Assertion

Ref	Expression
f1imaenfi	⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶)

Proof of Theorem f1imaenfi

Step	Hyp	Ref	Expression
1		f1ores 6711	. . . 4 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))
2		f1oenfi 8903	. . . . 5 ⊢ ((𝐶 ∈ Fin ∧ (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶)) → 𝐶 ≈ (𝐹 “ 𝐶))
3		ensymfib 8907	. . . . . 6 ⊢ (𝐶 ∈ Fin → (𝐶 ≈ (𝐹 “ 𝐶) ↔ (𝐹 “ 𝐶) ≈ 𝐶))
4	3	adantr 484	. . . . 5 ⊢ ((𝐶 ∈ Fin ∧ (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶)) → (𝐶 ≈ (𝐹 “ 𝐶) ↔ (𝐹 “ 𝐶) ≈ 𝐶))
5	2, 4	mpbid 235	. . . 4 ⊢ ((𝐶 ∈ Fin ∧ (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶)) → (𝐹 “ 𝐶) ≈ 𝐶)
6	1, 5	sylan2 596	. . 3 ⊢ ((𝐶 ∈ Fin ∧ (𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴)) → (𝐹 “ 𝐶) ≈ 𝐶)
7	6	3impb 1117	. 2 ⊢ ((𝐶 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ 𝐶) ≈ 𝐶)
8	7	3coml 1129	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   ∈ wcel 2112   ⊆ wss 3884   class class class wbr 5070   ↾ cres 5581   “ cima 5582  –1-1→wf1 6412  –1-1-onto→wf1o 6414   ≈ cen 8665  Fincfn 8668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346  ax-un 7563

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-om 7685  df-1o 8244  df-en 8669  df-fin 8672

This theorem is referenced by: (None)