fodomr

Description: There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006)

		Ref	Expression
	Assertion	fodomr	$⊢ (\emptyset ≺ B \land B ≼ A) \to \exists f f : A \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ B ≼ A \to A \in V$
3	2	adantl	$⊢ (\emptyset ≺ B \land B ≼ A) \to A \in V$
4	1	brrelex1i	$⊢ B ≼ A \to B \in V$
5		0sdomg	$⊢ B \in V \to (\emptyset ≺ B \leftrightarrow B \neq \emptyset)$
6		n0	$⊢ B \neq \emptyset \leftrightarrow \exists z z \in B$
7	5 6	bitrdi	$⊢ B \in V \to (\emptyset ≺ B \leftrightarrow \exists z z \in B)$
8	4 7	syl	$⊢ B ≼ A \to (\emptyset ≺ B \leftrightarrow \exists z z \in B)$
9	8	biimpac	$⊢ (\emptyset ≺ B \land B ≼ A) \to \exists z z \in B$
10		brdomi	$⊢ B ≼ A \to \exists g g : B \underset{1-1}{⟶} A$
11	10	adantl	$⊢ (\emptyset ≺ B \land B ≼ A) \to \exists g g : B \underset{1-1}{⟶} A$
12		difexg	$⊢ A \in V \to A ∖ ran g \in V$
13		snex	$⊢ \{z\} \in V$
14		xpexg	$⊢ (A ∖ ran g \in V \land \{z\} \in V) \to (A ∖ ran g) \times \{z\} \in V$
15	12 13 14	sylancl	$⊢ A \in V \to (A ∖ ran g) \times \{z\} \in V$
16		vex	$⊢ g \in V$
17	16	cnvex	$⊢ g^{-1} \in V$
18	15 17	jctil	$⊢ A \in V \to (g^{-1} \in V \land (A ∖ ran g) \times \{z\} \in V)$
19		unexb	$⊢ (g^{-1} \in V \land (A ∖ ran g) \times \{z\} \in V) \leftrightarrow g^{-1} \cup ((A ∖ ran g) \times \{z\}) \in V$
20	18 19	sylib	$⊢ A \in V \to g^{-1} \cup ((A ∖ ran g) \times \{z\}) \in V$
21		df-f1	$⊢ g : B \underset{1-1}{⟶} A \leftrightarrow (g : B ⟶ A \land Fun g^{-1})$
22	21	simprbi	$⊢ g : B \underset{1-1}{⟶} A \to Fun g^{-1}$
23		vex	$⊢ z \in V$
24	23	fconst	$⊢ ((A ∖ ran g) \times \{z\}) : A ∖ ran g ⟶ \{z\}$
25		ffun	$⊢ ((A ∖ ran g) \times \{z\}) : A ∖ ran g ⟶ \{z\} \to Fun ((A ∖ ran g) \times \{z\})$
26	24 25	ax-mp	$⊢ Fun ((A ∖ ran g) \times \{z\})$
27	22 26	jctir	$⊢ g : B \underset{1-1}{⟶} A \to (Fun g^{-1} \land Fun ((A ∖ ran g) \times \{z\}))$
28		df-rn	$⊢ ran g = dom g^{-1}$
29	28	eqcomi	$⊢ dom g^{-1} = ran g$
30	23	snnz	$⊢ \{z\} \neq \emptyset$
31		dmxp	$⊢ \{z\} \neq \emptyset \to dom ((A ∖ ran g) \times \{z\}) = A ∖ ran g$
32	30 31	ax-mp	$⊢ dom ((A ∖ ran g) \times \{z\}) = A ∖ ran g$
33	29 32	ineq12i	$⊢ dom g^{-1} \cap dom ((A ∖ ran g) \times \{z\}) = ran g \cap (A ∖ ran g)$
34		disjdif	$⊢ ran g \cap (A ∖ ran g) = \emptyset$
35	33 34	eqtri	$⊢ dom g^{-1} \cap dom ((A ∖ ran g) \times \{z\}) = \emptyset$
36		funun	$⊢ ((Fun g^{-1} \land Fun ((A ∖ ran g) \times \{z\})) \land dom g^{-1} \cap dom ((A ∖ ran g) \times \{z\}) = \emptyset) \to Fun (g^{-1} \cup ((A ∖ ran g) \times \{z\}))$
37	27 35 36	sylancl	$⊢ g : B \underset{1-1}{⟶} A \to Fun (g^{-1} \cup ((A ∖ ran g) \times \{z\}))$
38	37	adantl	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to Fun (g^{-1} \cup ((A ∖ ran g) \times \{z\}))$
39		dmun	$⊢ dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = dom g^{-1} \cup dom ((A ∖ ran g) \times \{z\})$
40	28	uneq1i	$⊢ ran g \cup dom ((A ∖ ran g) \times \{z\}) = dom g^{-1} \cup dom ((A ∖ ran g) \times \{z\})$
41	32	uneq2i	$⊢ ran g \cup dom ((A ∖ ran g) \times \{z\}) = ran g \cup (A ∖ ran g)$
42	39 40 41	3eqtr2i	$⊢ dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = ran g \cup (A ∖ ran g)$
43		f1f	$⊢ g : B \underset{1-1}{⟶} A \to g : B ⟶ A$
44	43	frnd	$⊢ g : B \underset{1-1}{⟶} A \to ran g \subseteq A$
45		undif	$⊢ ran g \subseteq A \leftrightarrow ran g \cup (A ∖ ran g) = A$
46	44 45	sylib	$⊢ g : B \underset{1-1}{⟶} A \to ran g \cup (A ∖ ran g) = A$
47	42 46	syl5eq	$⊢ g : B \underset{1-1}{⟶} A \to dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = A$
48	47	adantl	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = A$
49		df-fn	$⊢ (g^{-1} \cup ((A ∖ ran g) \times \{z\})) Fn A \leftrightarrow (Fun (g^{-1} \cup ((A ∖ ran g) \times \{z\})) \land dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = A)$
50	38 48 49	sylanbrc	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to (g^{-1} \cup ((A ∖ ran g) \times \{z\})) Fn A$
51		rnun	$⊢ ran (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = ran g^{-1} \cup ran ((A ∖ ran g) \times \{z\})$
52		dfdm4	$⊢ dom g = ran g^{-1}$
53		f1dm	$⊢ g : B \underset{1-1}{⟶} A \to dom g = B$
54	52 53	eqtr3id	$⊢ g : B \underset{1-1}{⟶} A \to ran g^{-1} = B$
55	54	uneq1d	$⊢ g : B \underset{1-1}{⟶} A \to ran g^{-1} \cup ran ((A ∖ ran g) \times \{z\}) = B \cup ran ((A ∖ ran g) \times \{z\})$
56		xpeq1	$⊢ A ∖ ran g = \emptyset \to (A ∖ ran g) \times \{z\} = \emptyset \times \{z\}$
57		0xp	$⊢ \emptyset \times \{z\} = \emptyset$
58	56 57	eqtrdi	$⊢ A ∖ ran g = \emptyset \to (A ∖ ran g) \times \{z\} = \emptyset$
59	58	rneqd	$⊢ A ∖ ran g = \emptyset \to ran ((A ∖ ran g) \times \{z\}) = ran \emptyset$
60		rn0	$⊢ ran \emptyset = \emptyset$
61	59 60	eqtrdi	$⊢ A ∖ ran g = \emptyset \to ran ((A ∖ ran g) \times \{z\}) = \emptyset$
62		0ss	$⊢ \emptyset \subseteq B$
63	61 62	eqsstrdi	$⊢ A ∖ ran g = \emptyset \to ran ((A ∖ ran g) \times \{z\}) \subseteq B$
64	63	a1d	$⊢ A ∖ ran g = \emptyset \to (z \in B \to ran ((A ∖ ran g) \times \{z\}) \subseteq B)$
65		rnxp	$⊢ A ∖ ran g \neq \emptyset \to ran ((A ∖ ran g) \times \{z\}) = \{z\}$
66	65	adantr	$⊢ (A ∖ ran g \neq \emptyset \land z \in B) \to ran ((A ∖ ran g) \times \{z\}) = \{z\}$
67		snssi	$⊢ z \in B \to \{z\} \subseteq B$
68	67	adantl	$⊢ (A ∖ ran g \neq \emptyset \land z \in B) \to \{z\} \subseteq B$
69	66 68	eqsstrd	$⊢ (A ∖ ran g \neq \emptyset \land z \in B) \to ran ((A ∖ ran g) \times \{z\}) \subseteq B$
70	69	ex	$⊢ A ∖ ran g \neq \emptyset \to (z \in B \to ran ((A ∖ ran g) \times \{z\}) \subseteq B)$
71	64 70	pm2.61ine	$⊢ z \in B \to ran ((A ∖ ran g) \times \{z\}) \subseteq B$
72		ssequn2	$⊢ ran ((A ∖ ran g) \times \{z\}) \subseteq B \leftrightarrow B \cup ran ((A ∖ ran g) \times \{z\}) = B$
73	71 72	sylib	$⊢ z \in B \to B \cup ran ((A ∖ ran g) \times \{z\}) = B$
74	55 73	sylan9eqr	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to ran g^{-1} \cup ran ((A ∖ ran g) \times \{z\}) = B$
75	51 74	syl5eq	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to ran (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = B$
76		df-fo	$⊢ (g^{-1} \cup ((A ∖ ran g) \times \{z\})) : A \underset{onto}{⟶} B \leftrightarrow ((g^{-1} \cup ((A ∖ ran g) \times \{z\})) Fn A \land ran (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = B)$
77	50 75 76	sylanbrc	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to (g^{-1} \cup ((A ∖ ran g) \times \{z\})) : A \underset{onto}{⟶} B$
78		foeq1	$⊢ f = g^{-1} \cup ((A ∖ ran g) \times \{z\}) \to (f : A \underset{onto}{⟶} B \leftrightarrow (g^{-1} \cup ((A ∖ ran g) \times \{z\})) : A \underset{onto}{⟶} B)$
79	78	spcegv	$⊢ g^{-1} \cup ((A ∖ ran g) \times \{z\}) \in V \to ((g^{-1} \cup ((A ∖ ran g) \times \{z\})) : A \underset{onto}{⟶} B \to \exists f f : A \underset{onto}{⟶} B)$
80	20 77 79	syl2im	$⊢ A \in V \to ((z \in B \land g : B \underset{1-1}{⟶} A) \to \exists f f : A \underset{onto}{⟶} B)$
81	80	expdimp	$⊢ (A \in V \land z \in B) \to (g : B \underset{1-1}{⟶} A \to \exists f f : A \underset{onto}{⟶} B)$
82	81	exlimdv	$⊢ (A \in V \land z \in B) \to (\exists g g : B \underset{1-1}{⟶} A \to \exists f f : A \underset{onto}{⟶} B)$
83	82	ex	$⊢ A \in V \to (z \in B \to (\exists g g : B \underset{1-1}{⟶} A \to \exists f f : A \underset{onto}{⟶} B))$
84	83	exlimdv	$⊢ A \in V \to (\exists z z \in B \to (\exists g g : B \underset{1-1}{⟶} A \to \exists f f : A \underset{onto}{⟶} B))$
85	3 9 11 84	syl3c	$⊢ (\emptyset ≺ B \land B ≼ A) \to \exists f f : A \underset{onto}{⟶} B$

Metamath Proof Explorer

Theorem fodomr

Proof