fodomfir

Description: There exists a mapping from a finite set onto any nonempty set that it dominates, proved without using the Axiom of Power Sets (unlike fodomr ). (Contributed by BTernaryTau, 23-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		relsdom	$⊢ Rel ≺$
2	1	brrelex2i	$⊢ \emptyset ≺ B \to B \in V$
3		0sdomg	$⊢ B \in V \to (\emptyset ≺ B \leftrightarrow B \neq \emptyset)$
4		n0	$⊢ B \neq \emptyset \leftrightarrow \exists z z \in B$
5	3 4	bitrdi	$⊢ B \in V \to (\emptyset ≺ B \leftrightarrow \exists z z \in B)$
6	2 5	syl	$⊢ \emptyset ≺ B \to (\emptyset ≺ B \leftrightarrow \exists z z \in B)$
7	6	ibi	$⊢ \emptyset ≺ B \to \exists z z \in B$
8		domfi	$⊢ (A \in Fin \land B ≼ A) \to B \in Fin$
9		simpl	$⊢ (A \in Fin \land B ≼ A) \to A \in Fin$
10		brdomi	$⊢ B ≼ A \to \exists g g : B \underset{1-1}{⟶} A$
11		f1fn	$⊢ g : B \underset{1-1}{⟶} A \to g Fn B$
12		fnfi	$⊢ (g Fn B \land B \in Fin) \to g \in Fin$
13	11 12	sylan	$⊢ (g : B \underset{1-1}{⟶} A \land B \in Fin) \to g \in Fin$
14	13	ex	$⊢ g : B \underset{1-1}{⟶} A \to (B \in Fin \to g \in Fin)$
15		cnvfi	$⊢ g \in Fin \to g^{-1} \in Fin$
16		diffi	$⊢ A \in Fin \to A ∖ ran g \in Fin$
17		snfi	$⊢ \{z\} \in Fin$
18		xpfi	$⊢ (A ∖ ran g \in Fin \land \{z\} \in Fin) \to (A ∖ ran g) \times \{z\} \in Fin$
19	16 17 18	sylancl	$⊢ A \in Fin \to (A ∖ ran g) \times \{z\} \in Fin$
20		unfi	$⊢ (g^{-1} \in Fin \land (A ∖ ran g) \times \{z\} \in Fin) \to g^{-1} \cup ((A ∖ ran g) \times \{z\}) \in Fin$
21	15 19 20	syl2an	$⊢ (g \in Fin \land A \in Fin) \to g^{-1} \cup ((A ∖ ran g) \times \{z\}) \in Fin$
22		df-f1	$⊢ g : B \underset{1-1}{⟶} A \leftrightarrow (g : B ⟶ A \land Fun g^{-1})$
23	22	simprbi	$⊢ g : B \underset{1-1}{⟶} A \to Fun g^{-1}$
24		vex	$⊢ z \in V$
25	24	fconst	$⊢ ((A ∖ ran g) \times \{z\}) : A ∖ ran g ⟶ \{z\}$
26		ffun	$⊢ ((A ∖ ran g) \times \{z\}) : A ∖ ran g ⟶ \{z\} \to Fun ((A ∖ ran g) \times \{z\})$
27	25 26	ax-mp	$⊢ Fun ((A ∖ ran g) \times \{z\})$
28	23 27	jctir	$⊢ g : B \underset{1-1}{⟶} A \to (Fun g^{-1} \land Fun ((A ∖ ran g) \times \{z\}))$
29		df-rn	$⊢ ran g = dom g^{-1}$
30	29	eqcomi	$⊢ dom g^{-1} = ran g$
31	24	snnz	$⊢ \{z\} \neq \emptyset$
32		dmxp	$⊢ \{z\} \neq \emptyset \to dom ((A ∖ ran g) \times \{z\}) = A ∖ ran g$
33	31 32	ax-mp	$⊢ dom ((A ∖ ran g) \times \{z\}) = A ∖ ran g$
34	30 33	ineq12i	$⊢ dom g^{-1} \cap dom ((A ∖ ran g) \times \{z\}) = ran g \cap (A ∖ ran g)$
35		disjdif	$⊢ ran g \cap (A ∖ ran g) = \emptyset$
36	34 35	eqtri	$⊢ dom g^{-1} \cap dom ((A ∖ ran g) \times \{z\}) = \emptyset$
37		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\}))$
38	28 36 37	sylancl	$⊢ g : B \underset{1-1}{⟶} A \to Fun (g^{-1} \cup ((A ∖ ran g) \times \{z\}))$
39	38	adantl	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to Fun (g^{-1} \cup ((A ∖ ran g) \times \{z\}))$
40		dmun	$⊢ dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = dom g^{-1} \cup dom ((A ∖ ran g) \times \{z\})$
41	29	uneq1i	$⊢ ran g \cup dom ((A ∖ ran g) \times \{z\}) = dom g^{-1} \cup dom ((A ∖ ran g) \times \{z\})$
42	33	uneq2i	$⊢ ran g \cup dom ((A ∖ ran g) \times \{z\}) = ran g \cup (A ∖ ran g)$
43	40 41 42	3eqtr2i	$⊢ dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = ran g \cup (A ∖ ran g)$
44		f1f	$⊢ g : B \underset{1-1}{⟶} A \to g : B ⟶ A$
45	44	frnd	$⊢ g : B \underset{1-1}{⟶} A \to ran g \subseteq A$
46		undif	$⊢ ran g \subseteq A \leftrightarrow ran g \cup (A ∖ ran g) = A$
47	45 46	sylib	$⊢ g : B \underset{1-1}{⟶} A \to ran g \cup (A ∖ ran g) = A$
48	43 47	eqtrid	$⊢ g : B \underset{1-1}{⟶} A \to dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = A$
49	48	adantl	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to dom (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = A$
50		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)$
51	39 49 50	sylanbrc	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to (g^{-1} \cup ((A ∖ ran g) \times \{z\})) Fn A$
52		rnun	$⊢ ran (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = ran g^{-1} \cup ran ((A ∖ ran g) \times \{z\})$
53		dfdm4	$⊢ dom g = ran g^{-1}$
54		f1dm	$⊢ g : B \underset{1-1}{⟶} A \to dom g = B$
55	53 54	eqtr3id	$⊢ g : B \underset{1-1}{⟶} A \to ran g^{-1} = B$
56	55	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\})$
57		xpeq1	$⊢ A ∖ ran g = \emptyset \to (A ∖ ran g) \times \{z\} = \emptyset \times \{z\}$
58		0xp	$⊢ \emptyset \times \{z\} = \emptyset$
59	57 58	eqtrdi	$⊢ A ∖ ran g = \emptyset \to (A ∖ ran g) \times \{z\} = \emptyset$
60	59	rneqd	$⊢ A ∖ ran g = \emptyset \to ran ((A ∖ ran g) \times \{z\}) = ran \emptyset$
61		rn0	$⊢ ran \emptyset = \emptyset$
62	60 61	eqtrdi	$⊢ A ∖ ran g = \emptyset \to ran ((A ∖ ran g) \times \{z\}) = \emptyset$
63		0ss	$⊢ \emptyset \subseteq B$
64	62 63	eqsstrdi	$⊢ A ∖ ran g = \emptyset \to ran ((A ∖ ran g) \times \{z\}) \subseteq B$
65	64	a1d	$⊢ A ∖ ran g = \emptyset \to (z \in B \to ran ((A ∖ ran g) \times \{z\}) \subseteq B)$
66		rnxp	$⊢ A ∖ ran g \neq \emptyset \to ran ((A ∖ ran g) \times \{z\}) = \{z\}$
67	66	adantr	$⊢ (A ∖ ran g \neq \emptyset \land z \in B) \to ran ((A ∖ ran g) \times \{z\}) = \{z\}$
68		snssi	$⊢ z \in B \to \{z\} \subseteq B$
69	68	adantl	$⊢ (A ∖ ran g \neq \emptyset \land z \in B) \to \{z\} \subseteq B$
70	67 69	eqsstrd	$⊢ (A ∖ ran g \neq \emptyset \land z \in B) \to ran ((A ∖ ran g) \times \{z\}) \subseteq B$
71	70	ex	$⊢ A ∖ ran g \neq \emptyset \to (z \in B \to ran ((A ∖ ran g) \times \{z\}) \subseteq B)$
72	65 71	pm2.61ine	$⊢ z \in B \to ran ((A ∖ ran g) \times \{z\}) \subseteq B$
73		ssequn2	$⊢ ran ((A ∖ ran g) \times \{z\}) \subseteq B \leftrightarrow B \cup ran ((A ∖ ran g) \times \{z\}) = B$
74	72 73	sylib	$⊢ z \in B \to B \cup ran ((A ∖ ran g) \times \{z\}) = B$
75	56 74	sylan9eqr	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to ran g^{-1} \cup ran ((A ∖ ran g) \times \{z\}) = B$
76	52 75	eqtrid	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to ran (g^{-1} \cup ((A ∖ ran g) \times \{z\})) = B$
77		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)$
78	51 76 77	sylanbrc	$⊢ (z \in B \land g : B \underset{1-1}{⟶} A) \to (g^{-1} \cup ((A ∖ ran g) \times \{z\})) : A \underset{onto}{⟶} B$
79		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)$
80	79	spcegv	$⊢ g^{-1} \cup ((A ∖ ran g) \times \{z\}) \in Fin \to ((g^{-1} \cup ((A ∖ ran g) \times \{z\})) : A \underset{onto}{⟶} B \to \exists f f : A \underset{onto}{⟶} B)$
81	21 78 80	syl2im	$⊢ (g \in Fin \land A \in Fin) \to ((z \in B \land g : B \underset{1-1}{⟶} A) \to \exists f f : A \underset{onto}{⟶} B)$
82	81	expcomd	$⊢ (g \in Fin \land A \in Fin) \to (g : B \underset{1-1}{⟶} A \to (z \in B \to \exists f f : A \underset{onto}{⟶} B))$
83	82	com12	$⊢ g : B \underset{1-1}{⟶} A \to ((g \in Fin \land A \in Fin) \to (z \in B \to \exists f f : A \underset{onto}{⟶} B))$
84	14 83	syland	$⊢ g : B \underset{1-1}{⟶} A \to ((B \in Fin \land A \in Fin) \to (z \in B \to \exists f f : A \underset{onto}{⟶} B))$
85	84	exlimiv	$⊢ \exists g g : B \underset{1-1}{⟶} A \to ((B \in Fin \land A \in Fin) \to (z \in B \to \exists f f : A \underset{onto}{⟶} B))$
86	10 85	syl	$⊢ B ≼ A \to ((B \in Fin \land A \in Fin) \to (z \in B \to \exists f f : A \underset{onto}{⟶} B))$
87	86	adantl	$⊢ (A \in Fin \land B ≼ A) \to ((B \in Fin \land A \in Fin) \to (z \in B \to \exists f f : A \underset{onto}{⟶} B))$
88	8 9 87	mp2and	$⊢ (A \in Fin \land B ≼ A) \to (z \in B \to \exists f f : A \underset{onto}{⟶} B)$
89	88	exlimdv	$⊢ (A \in Fin \land B ≼ A) \to (\exists z z \in B \to \exists f f : A \underset{onto}{⟶} B)$
90	7 89	syl5	$⊢ (A \in Fin \land B ≼ A) \to (\emptyset ≺ B \to \exists f f : A \underset{onto}{⟶} B)$
91	90	3impia	$⊢ (A \in Fin \land B ≼ A \land \emptyset ≺ B) \to \exists f f : A \underset{onto}{⟶} B$
92	91	3com23	$⊢ (A \in Fin \land \emptyset ≺ B \land B ≼ A) \to \exists f f : A \underset{onto}{⟶} B$

Metamath Proof Explorer

Theorem fodomfir

Proof