This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –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 vex ⊢ 𝑓 ∈ V
12 11 dmex ⊢ dom 𝑓 ∈ V
13 2 12 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐴 ∈ V )
14 focdmex ⊢ ( 𝐴 ∈ V → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )
15 13 14 mpcom ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V )
16 0sdomg ⊢ ( 𝐵 ∈ V → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) )
17 15 16 syl ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) )
18 17 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → ( ∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅ ) )
19 10 18 mpbird ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → ∅ ≺ 𝐵 )
20 19 ex ⊢ ( 𝐴 ≠ ∅ → ( 𝑓 : 𝐴 –onto→ 𝐵 → ∅ ≺ 𝐵 ) )
21 fodomg ⊢ ( 𝐴 ∈ V → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 ) )
22 13 21 mpcom ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ≼ 𝐴 )
23 20 22 jca2 ⊢ ( 𝐴 ≠ ∅ → ( 𝑓 : 𝐴 –onto→ 𝐵 → ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
24 23 exlimdv ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 → ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) ) )
25 24 imp ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) → ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) )
26 sdomdomtr ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∅ ≺ 𝐴 )
27 reldom ⊢ Rel ≼
28 27 brrelex2i ⊢ ( 𝐵 ≼ 𝐴 → 𝐴 ∈ V )
29 28 adantl ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ∈ V )
30 0sdomg ⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
31 29 30 syl ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
32 26 31 mpbid ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≠ ∅ )
33 fodomr ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 )
34 32 33 jca ⊢ ( ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) )
35 25 34 impbii ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ) ↔ ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) )