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 \in Fin \to ((A \neq \emptyset \land \exists f f : A \underset{onto}{⟶} B) \leftrightarrow (\emptyset ≺ B \land B ≼ A))$

Proof

Step	Hyp	Ref	Expression
1		fof	$⊢ f : A \underset{onto}{⟶} B \to f : A ⟶ B$
2	1	fdmd	$⊢ f : A \underset{onto}{⟶} B \to dom f = A$
3	2	eqeq1d	$⊢ f : A \underset{onto}{⟶} B \to (dom f = \emptyset \leftrightarrow A = \emptyset)$
4		dm0rn0	$⊢ dom f = \emptyset \leftrightarrow ran f = \emptyset$
5		forn	$⊢ f : A \underset{onto}{⟶} B \to ran f = B$
6	5	eqeq1d	$⊢ f : A \underset{onto}{⟶} B \to (ran f = \emptyset \leftrightarrow B = \emptyset)$
7	4 6	bitrid	$⊢ f : A \underset{onto}{⟶} B \to (dom f = \emptyset \leftrightarrow B = \emptyset)$
8	3 7	bitr3d	$⊢ f : A \underset{onto}{⟶} B \to (A = \emptyset \leftrightarrow B = \emptyset)$
9	8	necon3bid	$⊢ f : A \underset{onto}{⟶} B \to (A \neq \emptyset \leftrightarrow B \neq \emptyset)$
10	9	biimpac	$⊢ (A \neq \emptyset \land f : A \underset{onto}{⟶} B) \to B \neq \emptyset$
11	10	adantll	$⊢ ((A \in Fin \land A \neq \emptyset) \land f : A \underset{onto}{⟶} B) \to B \neq \emptyset$
12		vex	$⊢ f \in V$
13	12	rnex	$⊢ ran f \in V$
14	5 13	eqeltrrdi	$⊢ f : A \underset{onto}{⟶} B \to B \in V$
15	14	adantl	$⊢ (A \in Fin \land f : A \underset{onto}{⟶} B) \to B \in V$
16		0sdomg	$⊢ B \in V \to (\emptyset ≺ B \leftrightarrow B \neq \emptyset)$
17	15 16	syl	$⊢ (A \in Fin \land f : A \underset{onto}{⟶} B) \to (\emptyset ≺ B \leftrightarrow B \neq \emptyset)$
18	17	adantlr	$⊢ ((A \in Fin \land A \neq \emptyset) \land f : A \underset{onto}{⟶} B) \to (\emptyset ≺ B \leftrightarrow B \neq \emptyset)$
19	11 18	mpbird	$⊢ ((A \in Fin \land A \neq \emptyset) \land f : A \underset{onto}{⟶} B) \to \emptyset ≺ B$
20	19	ex	$⊢ (A \in Fin \land A \neq \emptyset) \to (f : A \underset{onto}{⟶} B \to \emptyset ≺ B)$
21		fodomfi	$⊢ (A \in Fin \land f : A \underset{onto}{⟶} B) \to B ≼ A$
22	21	ex	$⊢ A \in Fin \to (f : A \underset{onto}{⟶} B \to B ≼ A)$
23	22	adantr	$⊢ (A \in Fin \land A \neq \emptyset) \to (f : A \underset{onto}{⟶} B \to B ≼ A)$
24	20 23	jcad	$⊢ (A \in Fin \land A \neq \emptyset) \to (f : A \underset{onto}{⟶} B \to (\emptyset ≺ B \land B ≼ A))$
25	24	exlimdv	$⊢ (A \in Fin \land A \neq \emptyset) \to (\exists f f : A \underset{onto}{⟶} B \to (\emptyset ≺ B \land B ≼ A))$
26	25	expimpd	$⊢ A \in Fin \to ((A \neq \emptyset \land \exists f f : A \underset{onto}{⟶} B) \to (\emptyset ≺ B \land B ≼ A))$
27		sdomdomtr	$⊢ (\emptyset ≺ B \land B ≼ A) \to \emptyset ≺ A$
28		0sdomg	$⊢ A \in Fin \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
29	27 28	imbitrid	$⊢ A \in Fin \to ((\emptyset ≺ B \land B ≼ A) \to A \neq \emptyset)$
30		fodomr	$⊢ (\emptyset ≺ B \land B ≼ A) \to \exists f f : A \underset{onto}{⟶} B$
31	29 30	jca2	$⊢ A \in Fin \to ((\emptyset ≺ B \land B ≼ A) \to (A \neq \emptyset \land \exists f f : A \underset{onto}{⟶} B))$
32	26 31	impbid	$⊢ A \in Fin \to ((A \neq \emptyset \land \exists f f : A \underset{onto}{⟶} B) \leftrightarrow (\emptyset ≺ B \land B ≼ A))$

Metamath Proof Explorer

Theorem fodomfib

Proof