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 ⊢ A ∈ Fin → A ≠ ∅ ∧ ∃ f f : A ⟶ onto B ↔ ∅ ≺ B ∧ B ≼ A

Proof

Step Hyp Ref Expression
1 fof ⊢ f : A ⟶ onto B → f : A ⟶ B
2 1 fdmd ⊢ f : A ⟶ onto B → dom ⁡ f = A
3 2 eqeq1d ⊢ f : A ⟶ onto B → dom ⁡ f = ∅ ↔ A = ∅
4 dm0rn0 ⊢ dom ⁡ f = ∅ ↔ ran ⁡ f = ∅
5 forn ⊢ f : A ⟶ onto B → ran ⁡ f = B
6 5 eqeq1d ⊢ f : A ⟶ onto B → ran ⁡ f = ∅ ↔ B = ∅
7 4 6 syl5bb ⊢ f : A ⟶ onto B → dom ⁡ f = ∅ ↔ B = ∅
8 3 7 bitr3d ⊢ f : A ⟶ onto B → A = ∅ ↔ B = ∅
9 8 necon3bid ⊢ f : A ⟶ onto B → A ≠ ∅ ↔ B ≠ ∅
10 9 biimpac ⊢ A ≠ ∅ ∧ f : A ⟶ onto B → B ≠ ∅
11 10 adantll ⊢ A ∈ Fin ∧ A ≠ ∅ ∧ f : A ⟶ onto B → B ≠ ∅
12 vex ⊢ f ∈ V
13 12 rnex ⊢ ran ⁡ f ∈ V
14 5 13 eqeltrrdi ⊢ f : A ⟶ onto B → B ∈ V
15 14 adantl ⊢ A ∈ Fin ∧ f : A ⟶ onto B → B ∈ V
16 0sdomg ⊢ B ∈ V → ∅ ≺ B ↔ B ≠ ∅
17 15 16 syl ⊢ A ∈ Fin ∧ f : A ⟶ onto B → ∅ ≺ B ↔ B ≠ ∅
18 17 adantlr ⊢ A ∈ Fin ∧ A ≠ ∅ ∧ f : A ⟶ onto B → ∅ ≺ B ↔ B ≠ ∅
19 11 18 mpbird ⊢ A ∈ Fin ∧ A ≠ ∅ ∧ f : A ⟶ onto B → ∅ ≺ B
20 19 ex ⊢ A ∈ Fin ∧ A ≠ ∅ → f : A ⟶ onto B → ∅ ≺ B
21 fodomfi ⊢ A ∈ Fin ∧ f : A ⟶ onto B → B ≼ A
22 21 ex ⊢ A ∈ Fin → f : A ⟶ onto B → B ≼ A
23 22 adantr ⊢ A ∈ Fin ∧ A ≠ ∅ → f : A ⟶ onto B → B ≼ A
24 20 23 jcad ⊢ A ∈ Fin ∧ A ≠ ∅ → f : A ⟶ onto B → ∅ ≺ B ∧ B ≼ A
25 24 exlimdv ⊢ A ∈ Fin ∧ A ≠ ∅ → ∃ f f : A ⟶ onto B → ∅ ≺ B ∧ B ≼ A
26 25 expimpd ⊢ A ∈ Fin → A ≠ ∅ ∧ ∃ f f : A ⟶ onto B → ∅ ≺ B ∧ B ≼ A
27 sdomdomtr ⊢ ∅ ≺ B ∧ B ≼ A → ∅ ≺ A
28 0sdomg ⊢ A ∈ Fin → ∅ ≺ A ↔ A ≠ ∅
29 27 28 syl5ib ⊢ A ∈ Fin → ∅ ≺ B ∧ B ≼ A → A ≠ ∅
30 fodomr ⊢ ∅ ≺ B ∧ B ≼ A → ∃ f f : A ⟶ onto B
31 29 30 jca2 ⊢ A ∈ Fin → ∅ ≺ B ∧ B ≼ A → A ≠ ∅ ∧ ∃ f f : A ⟶ onto B
32 26 31 impbid ⊢ A ∈ Fin → A ≠ ∅ ∧ ∃ f f : A ⟶ onto B ↔ ∅ ≺ B ∧ B ≼ A