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→ 𝐵 ) ↔ ( ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴 ) )