numwdom

Description: A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	numwdom	$⊢ (A \in dom card \land B ≼^{*} A) \to B \in dom card$

Step	Hyp	Ref	Expression
1		brwdomi	$⊢ B ≼^{*} A \to (B = \emptyset \lor \exists f f : A \underset{onto}{⟶} B)$
2		simpr	$⊢ (A \in dom card \land B = \emptyset) \to B = \emptyset$
3		0fin	$⊢ \emptyset \in Fin$
4		finnum	$⊢ \emptyset \in Fin \to \emptyset \in dom card$
5	3 4	ax-mp	$⊢ \emptyset \in dom card$
6	2 5	eqeltrdi	$⊢ (A \in dom card \land B = \emptyset) \to B \in dom card$
7		fonum	$⊢ (A \in dom card \land f : A \underset{onto}{⟶} B) \to B \in dom card$
8	7	ex	$⊢ A \in dom card \to (f : A \underset{onto}{⟶} B \to B \in dom card)$
9	8	exlimdv	$⊢ A \in dom card \to (\exists f f : A \underset{onto}{⟶} B \to B \in dom card)$
10	9	imp	$⊢ (A \in dom card \land \exists f f : A \underset{onto}{⟶} B) \to B \in dom card$
11	6 10	jaodan	$⊢ (A \in dom card \land (B = \emptyset \lor \exists f f : A \underset{onto}{⟶} B)) \to B \in dom card$
12	1 11	sylan2	$⊢ (A \in dom card \land B ≼^{*} A) \to B \in dom card$

Metamath Proof Explorer