Metamath Proof Explorer

Theorem fodomb

Description: Equivalence of an onto mapping and dominance for a nonempty set. Proposition 10.35 of TakeutiZaring p. 93. (Contributed by NM, 29-Jul-2004)

Ref Expression
Assertion fodomb ⊢ 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 vex ⊢ f ∈ V
12 11 dmex ⊢ dom ⁡ f ∈ V
13 2 12 syl6eqelr ⊢ f : A ⟶ onto B → A ∈ V
14 fornex ⊢ A ∈ V → f : A ⟶ onto B → B ∈ V
15 13 14 mpcom ⊢ f : A ⟶ onto B → B ∈ V
16 0sdomg ⊢ B ∈ V → ∅ ≺ B ↔ B ≠ ∅
17 15 16 syl ⊢ f : A ⟶ onto B → ∅ ≺ B ↔ B ≠ ∅
18 17 adantl ⊢ A ≠ ∅ ∧ f : A ⟶ onto B → ∅ ≺ B ↔ B ≠ ∅
19 10 18 mpbird ⊢ A ≠ ∅ ∧ f : A ⟶ onto B → ∅ ≺ B
20 19 ex ⊢ A ≠ ∅ → f : A ⟶ onto B → ∅ ≺ B
21 fodomg ⊢ A ∈ V → f : A ⟶ onto B → B ≼ A
22 13 21 mpcom ⊢ f : A ⟶ onto B → B ≼ A
23 20 22 jca2 ⊢ A ≠ ∅ → f : A ⟶ onto B → ∅ ≺ B ∧ B ≼ A
24 23 exlimdv ⊢ A ≠ ∅ → ∃ f f : A ⟶ onto B → ∅ ≺ B ∧ B ≼ A
25 24 imp ⊢ A ≠ ∅ ∧ ∃ f f : A ⟶ onto B → ∅ ≺ B ∧ B ≼ A
26 sdomdomtr ⊢ ∅ ≺ B ∧ B ≼ A → ∅ ≺ A
27 reldom ⊢ Rel ⁡ ≼
28 27 brrelex2i ⊢ B ≼ A → A ∈ V
29 28 adantl ⊢ ∅ ≺ B ∧ B ≼ A → A ∈ V
30 0sdomg ⊢ A ∈ V → ∅ ≺ A ↔ A ≠ ∅
31 29 30 syl ⊢ ∅ ≺ B ∧ B ≼ A → ∅ ≺ A ↔ A ≠ ∅
32 26 31 mpbid ⊢ ∅ ≺ B ∧ B ≼ A → A ≠ ∅
33 fodomr ⊢ ∅ ≺ B ∧ B ≼ A → ∃ f f : A ⟶ onto B
34 32 33 jca ⊢ ∅ ≺ B ∧ B ≼ A → A ≠ ∅ ∧ ∃ f f : A ⟶ onto B
35 25 34 impbii ⊢ A ≠ ∅ ∧ ∃ f f : A ⟶ onto B ↔ ∅ ≺ B ∧ B ≼ A