fodomfi

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodomg for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) (Proof shortened by Mario Carneiro, 16-Nov-2014) Avoid ax-pow . (Revised by BTernaryTau, 20-Jun-2025)

		Ref	Expression
	Assertion	fodomfi	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to B ≼ A$

Proof

Step	Hyp	Ref	Expression
1		foima	$⊢ F : A \underset{onto}{⟶} B \to F [A] = B$
2	1	adantl	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to F [A] = B$
3		imaeq2	$⊢ x = \emptyset \to F [x] = F [\emptyset]$
4		ima0	$⊢ F [\emptyset] = \emptyset$
5	3 4	eqtrdi	$⊢ x = \emptyset \to F [x] = \emptyset$
6		id	$⊢ x = \emptyset \to x = \emptyset$
7	5 6	breq12d	$⊢ x = \emptyset \to (F [x] ≼ x \leftrightarrow \emptyset ≼ \emptyset)$
8	7	imbi2d	$⊢ x = \emptyset \to ((F Fn A \to F [x] ≼ x) \leftrightarrow (F Fn A \to \emptyset ≼ \emptyset))$
9		imaeq2	$⊢ x = y \to F [x] = F [y]$
10		id	$⊢ x = y \to x = y$
11	9 10	breq12d	$⊢ x = y \to (F [x] ≼ x \leftrightarrow F [y] ≼ y)$
12	11	imbi2d	$⊢ x = y \to ((F Fn A \to F [x] ≼ x) \leftrightarrow (F Fn A \to F [y] ≼ y))$
13		imaeq2	$⊢ x = y \cup \{z\} \to F [x] = F [y \cup \{z\}]$
14		id	$⊢ x = y \cup \{z\} \to x = y \cup \{z\}$
15	13 14	breq12d	$⊢ x = y \cup \{z\} \to (F [x] ≼ x \leftrightarrow F [y \cup \{z\}] ≼ (y \cup \{z\}))$
16	15	imbi2d	$⊢ x = y \cup \{z\} \to ((F Fn A \to F [x] ≼ x) \leftrightarrow (F Fn A \to F [y \cup \{z\}] ≼ (y \cup \{z\})))$
17		imaeq2	$⊢ x = A \to F [x] = F [A]$
18		id	$⊢ x = A \to x = A$
19	17 18	breq12d	$⊢ x = A \to (F [x] ≼ x \leftrightarrow F [A] ≼ A)$
20	19	imbi2d	$⊢ x = A \to ((F Fn A \to F [x] ≼ x) \leftrightarrow (F Fn A \to F [A] ≼ A))$
21		0ex	$⊢ \emptyset \in V$
22	21	0dom	$⊢ \emptyset ≼ \emptyset$
23	22	a1i	$⊢ F Fn A \to \emptyset ≼ \emptyset$
24		fnfun	$⊢ F Fn A \to Fun F$
25	24	ad2antrl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to Fun F$
26		funressn	$⊢ Fun F \to {F ↾}_{\{z\}} \subseteq \{⟨z, F (z)⟩\}$
27		rnss	$⊢ {F ↾}_{\{z\}} \subseteq \{⟨z, F (z)⟩\} \to ran ({F ↾}_{\{z\}}) \subseteq ran \{⟨z, F (z)⟩\}$
28	25 26 27	3syl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to ran ({F ↾}_{\{z\}}) \subseteq ran \{⟨z, F (z)⟩\}$
29		df-ima	$⊢ F [\{z\}] = ran ({F ↾}_{\{z\}})$
30		vex	$⊢ z \in V$
31	30	rnsnop	$⊢ ran \{⟨z, F (z)⟩\} = \{F (z)\}$
32	31	eqcomi	$⊢ \{F (z)\} = ran \{⟨z, F (z)⟩\}$
33	28 29 32	3sstr4g	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [\{z\}] \subseteq \{F (z)\}$
34		snfi	$⊢ \{F (z)\} \in Fin$
35		ssexg	$⊢ (F [\{z\}] \subseteq \{F (z)\} \land \{F (z)\} \in Fin) \to F [\{z\}] \in V$
36	33 34 35	sylancl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [\{z\}] \in V$
37		fvi	$⊢ F [\{z\}] \in V \to I (F [\{z\}]) = F [\{z\}]$
38	36 37	syl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to I (F [\{z\}]) = F [\{z\}]$
39	38	uneq2d	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [y] \cup I (F [\{z\}]) = F [y] \cup F [\{z\}]$
40		imaundi	$⊢ F [y \cup \{z\}] = F [y] \cup F [\{z\}]$
41	39 40	eqtr4di	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [y] \cup I (F [\{z\}]) = F [y \cup \{z\}]$
42		simprr	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [y] ≼ y$
43		ssdomfi	$⊢ \{F (z)\} \in Fin \to (F [\{z\}] \subseteq \{F (z)\} \to F [\{z\}] ≼ \{F (z)\})$
44	34 33 43	mpsyl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [\{z\}] ≼ \{F (z)\}$
45		fvex	$⊢ F (z) \in V$
46		en2sn	$⊢ (F (z) \in V \land z \in V) \to \{F (z)\} \approx \{z\}$
47	45 30 46	mp2an	$⊢ \{F (z)\} \approx \{z\}$
48		endom	$⊢ \{F (z)\} \approx \{z\} \to \{F (z)\} ≼ \{z\}$
49		domtrfi	$⊢ (\{F (z)\} \in Fin \land F [\{z\}] ≼ \{F (z)\} \land \{F (z)\} ≼ \{z\}) \to F [\{z\}] ≼ \{z\}$
50	34 49	mp3an1	$⊢ (F [\{z\}] ≼ \{F (z)\} \land \{F (z)\} ≼ \{z\}) \to F [\{z\}] ≼ \{z\}$
51	48 50	sylan2	$⊢ (F [\{z\}] ≼ \{F (z)\} \land \{F (z)\} \approx \{z\}) \to F [\{z\}] ≼ \{z\}$
52	44 47 51	sylancl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [\{z\}] ≼ \{z\}$
53	38 52	eqbrtrd	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to I (F [\{z\}]) ≼ \{z\}$
54		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to \neg z \in y$
55		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
56	54 55	sylibr	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to y \cap \{z\} = \emptyset$
57		undom	$⊢ ((F [y] ≼ y \land I (F [\{z\}]) ≼ \{z\}) \land y \cap \{z\} = \emptyset) \to (F [y] \cup I (F [\{z\}])) ≼ (y \cup \{z\})$
58	42 53 56 57	syl21anc	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to (F [y] \cup I (F [\{z\}])) ≼ (y \cup \{z\})$
59	41 58	eqbrtrrd	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [y \cup \{z\}] ≼ (y \cup \{z\})$
60	59	exp32	$⊢ (y \in Fin \land \neg z \in y) \to (F Fn A \to (F [y] ≼ y \to F [y \cup \{z\}] ≼ (y \cup \{z\})))$
61	60	a2d	$⊢ (y \in Fin \land \neg z \in y) \to ((F Fn A \to F [y] ≼ y) \to (F Fn A \to F [y \cup \{z\}] ≼ (y \cup \{z\})))$
62	8 12 16 20 23 61	findcard2s	$⊢ A \in Fin \to (F Fn A \to F [A] ≼ A)$
63		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
64	62 63	impel	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to F [A] ≼ A$
65	2 64	eqbrtrrd	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to B ≼ A$

Metamath Proof Explorer

Theorem fodomfi

Proof