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 Choice for its proof. (Contributed by NM, 23-Mar-2006)

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 sdomdomtr ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∅ ≺ 𝐴 )
28 0sdomg ⊢ ( 𝐴 ∈ Fin → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
29 27 28 syl5ib ⊢ ( 𝐴 ∈ Fin → ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≠ ∅ ) )
30 fodomr ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 )
31 29 30 jca2 ⊢ ( 𝐴 ∈ Fin → ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ) )
32 26 31 impbid ⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ↔ ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )