fodomfi

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) (Proof shortened by Mario Carneiro, 16-Nov-2014)

		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		snex	$⊢ \{F (z)\} \in V$
35		ssexg	$⊢ (F [\{z\}] \subseteq \{F (z)\} \land \{F (z)\} \in V) \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		ssdomg	$⊢ \{F (z)\} \in V \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	45	ensn1	$⊢ \{F (z)\} \approx 1_{𝑜}$
47	30	ensn1	$⊢ \{z\} \approx 1_{𝑜}$
48	46 47	entr4i	$⊢ \{F (z)\} \approx \{z\}$
49		domentr	$⊢ (F [\{z\}] ≼ \{F (z)\} \land \{F (z)\} \approx \{z\}) \to F [\{z\}] ≼ \{z\}$
50	44 48 49	sylancl	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to F [\{z\}] ≼ \{z\}$
51	38 50	eqbrtrd	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to I (F [\{z\}]) ≼ \{z\}$
52		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to \neg z \in y$
53		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
54	52 53	sylibr	$⊢ ((y \in Fin \land \neg z \in y) \land (F Fn A \land F [y] ≼ y)) \to y \cap \{z\} = \emptyset$
55		undom	$⊢ ((F [y] ≼ y \land I (F [\{z\}]) ≼ \{z\}) \land y \cap \{z\} = \emptyset) \to (F [y] \cup I (F [\{z\}])) ≼ (y \cup \{z\})$
56	42 51 54 55	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\})$
57	41 56	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\})$
58	57	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\})))$
59	58	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\})))$
60	8 12 16 20 23 59	findcard2s	$⊢ A \in Fin \to (F Fn A \to F [A] ≼ A)$
61		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
62	60 61	impel	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to F [A] ≼ A$
63	2 62	eqbrtrrd	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to B ≼ A$

Metamath Proof Explorer

Theorem fodomfi

Proof