Metamath Proof Explorer

Theorem fodomfib

Description: Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) Avoid ax-pow . (Revised by BTernaryTau, 23-Jun-2025)

Ref Expression
Assertion fodomfib ( 𝐴 ∈ Fin → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ↔ ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fof ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
2 1 fdmd ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → dom 𝑓 = 𝐴 )
3 2 eqeq1d ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( dom 𝑓 = ∅ ↔ 𝐴 = ∅ ) )
4 dm0rn0 ⊢ ( dom 𝑓 = ∅ ↔ ran 𝑓 = ∅ )
5 forn ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ran 𝑓 = 𝐵 )
6 5 eqeq1d ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( ran 𝑓 = ∅ ↔ 𝐵 = ∅ ) )
7 4 6 bitrid ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( dom 𝑓 = ∅ ↔ 𝐵 = ∅ ) )
8 3 7 bitr3d ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( 𝐴 = ∅ ↔ 𝐵 = ∅ ) )
9 8 necon3bid ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( 𝐴 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
10 9 biimpac ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≠ ∅ )
11 10 adantll ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≠ ∅ )
12 vex ⊢ 𝑓 ∈ V
13 12 rnex ⊢ ran 𝑓 ∈ V
14 5 13 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V )
15 14 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ V )
16 0sdomg ⊢ ( 𝐵 ∈ V → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) )
17 15 16 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) )
18 17 adantlr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) )
19 11 18 mpbird ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → ∅ ≺ 𝐵 )
20 19 ex ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝑓 : 𝐴 –onto→ 𝐵 → ∅ ≺ 𝐵 ) )
21 fodomfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )
22 21 ex ⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 ) )
23 22 adantr ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 ) )
24 20 23 jcad ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝑓 : 𝐴 –onto→ 𝐵 → ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
25 24 exlimdv ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 → ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
26 25 expimpd ⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) → ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
27 0fi ⊢ ∅ ∈ Fin
28 sdomdomtrfi ⊢ ( ( ∅ ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∅ ≺ 𝐴 )
29 27 28 mp3an1 ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∅ ≺ 𝐴 )
30 0sdomg ⊢ ( 𝐴 ∈ Fin → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
31 29 30 imbitrid ⊢ ( 𝐴 ∈ Fin → ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≠ ∅ ) )
32 fodomfir ⊢ ( ( 𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 )
33 32 3expib ⊢ ( 𝐴 ∈ Fin → ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) )
34 31 33 jcad ⊢ ( 𝐴 ∈ Fin → ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) )
35 26 34 impbid ⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ↔ ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )