Theorem f1finf1o 9269

Description: Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) Avoid ax-pow 5326. (Revised by BTernaryTau, 4-Jan-2025.)

Assertion

Ref	Expression
f1finf1o	⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))

Proof of Theorem f1finf1o

Step	Hyp	Ref	Expression
1		simpr 490	. . . 4 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1→𝐵)
2		f1f 6781	. . . . . . 7 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	adantl 487	. . . . . 6 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴⟶𝐵)
4	3	ffnd 6713	. . . . 5 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹 Fn 𝐴)
5		simpll 779	. . . . . 6 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≈ 𝐵)
6	3	frnd 6721	. . . . . . . . 9 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → ran 𝐹 ⊆ 𝐵)
7		df-pss 4013	. . . . . . . . . 10 ⊢ (ran 𝐹 ⊊ 𝐵 ↔ (ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ≠ 𝐵))
8	7	baib 545	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ 𝐵 → (ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵))
9	6, 8	syl 18	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵))
10		php3 9229	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ ran 𝐹 ⊊ 𝐵) → ran 𝐹 ≺ 𝐵)
11	10	ex 418	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → (ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵))
12	11	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵))
13		enfii 9206	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
14	13	ancoms 464	. . . . . . . . . . 11 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin)
15		f1f1orn 6839	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
16		f1oenfi 9199	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→ran 𝐹) → 𝐴 ≈ ran 𝐹)
17	14, 15, 16	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≈ ran 𝐹)
18		endom 9011	. . . . . . . . . . . . 13 ⊢ (𝐴 ≈ ran 𝐹 → 𝐴 ≼ ran 𝐹)
19		domsdomtrfi 9222	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵) → 𝐴 ≺ 𝐵)
20	18, 19	syl3an2 1182	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵) → 𝐴 ≺ 𝐵)
21	20	3expia 1139	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ ran 𝐹) → (ran 𝐹 ≺ 𝐵 → 𝐴 ≺ 𝐵))
22	14, 17, 21	syl2an2r 698	. . . . . . . . . 10 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ≺ 𝐵 → 𝐴 ≺ 𝐵))
23	12, 22	syld 48	. . . . . . . . 9 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → 𝐴 ≺ 𝐵))
24		sdomnen 9013	. . . . . . . . 9 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
25	23, 24	syl6 36	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → ¬ 𝐴 ≈ 𝐵))
26	9, 25	sylbird 263	. . . . . . 7 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ≠ 𝐵 → ¬ 𝐴 ≈ 𝐵))
27	26	necon4ad 2974	. . . . . 6 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (𝐴 ≈ 𝐵 → ran 𝐹 = 𝐵))
28	5, 27	mpd 16	. . . . 5 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → ran 𝐹 = 𝐵)
29		df-fo 6547	. . . . 5 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
30	4, 28, 29	sylanbrc 595	. . . 4 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–onto→𝐵)
31		df-f1o 6548	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
32	1, 30, 31	sylanbrc 595	. . 3 ⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
33	32	ex 418	. 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→𝐵))
34		f1of1 6826	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
35	33, 34	impbid1 228	1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ≠ wne 2955   ⊆ wss 3896   ⊊ wpss 4012   class class class wbr 5102  ran crn 5651   Fn wfn 6536  ⟶wf 6537  –1-1→wf1 6538  –onto→wfo 6539  –1-1-onto→wf1o 6540   ≈ cen 8975   ≼ cdom 8976   ≺ csdm 8977  Fincfn 8978

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-om 7880  df-1o 8481  df-en 8979  df-dom 8980  df-sdom 8981  df-fin 8982

This theorem is used by:  hashfac  14608  crth  16962  eulerthlem2  16966  fidomndrnglem  21037  mdetunilem8  22941  basellem4  27418  lgsqrlem4  27683  lgseisenlem2  27710  aks5lem7  43357