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≠∅∧∃ff:A⟶ontoB↔∅≺B∧B≼A

Proof

Step Hyp Ref Expression
1 fof ⊢f:A⟶ontoB→f:A⟶B
2 1 fdmd ⊢f:A⟶ontoB→dom⁡f=A
3 2 eqeq1d ⊢f:A⟶ontoB→dom⁡f=∅↔A=∅
4 dm0rn0 ⊢dom⁡f=∅↔ran⁡f=∅
5 forn ⊢f:A⟶ontoB→ran⁡f=B
6 5 eqeq1d ⊢f:A⟶ontoB→ran⁡f=∅↔B=∅
7 4 6 bitrid ⊢f:A⟶ontoB→dom⁡f=∅↔B=∅
8 3 7 bitr3d ⊢f:A⟶ontoB→A=∅↔B=∅
9 8 necon3bid ⊢f:A⟶ontoB→A≠∅↔B≠∅
10 9 biimpac ⊢A≠∅∧f:A⟶ontoB→B≠∅
11 vex ⊢f∈V
12 11 dmex ⊢dom⁡f∈V
13 2 12 eqeltrrdi ⊢f:A⟶ontoB→A∈V
14 focdmex ⊢A∈V→f:A⟶ontoB→B∈V
15 13 14 mpcom ⊢f:A⟶ontoB→B∈V
16 0sdomg ⊢B∈V→∅≺B↔B≠∅
17 15 16 syl ⊢f:A⟶ontoB→∅≺B↔B≠∅
18 17 adantl ⊢A≠∅∧f:A⟶ontoB→∅≺B↔B≠∅
19 10 18 mpbird ⊢A≠∅∧f:A⟶ontoB→∅≺B
20 19 ex ⊢A≠∅→f:A⟶ontoB→∅≺B
21 fodomg ⊢A∈V→f:A⟶ontoB→B≼A
22 13 21 mpcom ⊢f:A⟶ontoB→B≼A
23 20 22 jca2 ⊢A≠∅→f:A⟶ontoB→∅≺B∧B≼A
24 23 exlimdv ⊢A≠∅→∃ff:A⟶ontoB→∅≺B∧B≼A
25 24 imp ⊢A≠∅∧∃ff:A⟶ontoB→∅≺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→∃ff:A⟶ontoB
34 32 33 jca ⊢∅≺B∧B≼A→A≠∅∧∃ff:A⟶ontoB
35 25 34 impbii ⊢A≠∅∧∃ff:A⟶ontoB↔∅≺B∧B≼A