fofinf1o

Description: Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014)

		Ref	Expression
	Assertion	fofinf1o	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to F : A \underset{onto}{⟶} B$
2		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
3	1 2	syl	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to F : A ⟶ B$
4		domnsym	$⊢ B ≼ (A ∖ \{y\}) \to \neg (A ∖ \{y\}) ≺ B$
5		simp3	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to B \in Fin$
6		simp2	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to A \approx B$
7		enfii	$⊢ (B \in Fin \land A \approx B) \to A \in Fin$
8	5 6 7	syl2anc	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to A \in Fin$
9	8	ad2antrr	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to A \in Fin$
10		difssd	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to A ∖ \{y\} \subseteq A$
11		simplrr	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to y \in A$
12		neldifsn	$⊢ \neg y \in (A ∖ \{y\})$
13		nelne1	$⊢ (y \in A \land \neg y \in (A ∖ \{y\})) \to A \neq A ∖ \{y\}$
14	11 12 13	sylancl	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to A \neq A ∖ \{y\}$
15	14	necomd	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to A ∖ \{y\} \neq A$
16		df-pss	$⊢ A ∖ \{y\} \subset A \leftrightarrow (A ∖ \{y\} \subseteq A \land A ∖ \{y\} \neq A)$
17	10 15 16	sylanbrc	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to A ∖ \{y\} \subset A$
18		php3	$⊢ (A \in Fin \land A ∖ \{y\} \subset A) \to (A ∖ \{y\}) ≺ A$
19	9 17 18	syl2anc	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to (A ∖ \{y\}) ≺ A$
20	6	ad2antrr	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to A \approx B$
21		sdomentr	$⊢ ((A ∖ \{y\}) ≺ A \land A \approx B) \to (A ∖ \{y\}) ≺ B$
22	19 20 21	syl2anc	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to (A ∖ \{y\}) ≺ B$
23	4 22	nsyl3	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to \neg B ≼ (A ∖ \{y\})$
24	8	adantr	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to A \in Fin$
25		difss	$⊢ A ∖ \{y\} \subseteq A$
26		ssfi	$⊢ (A \in Fin \land A ∖ \{y\} \subseteq A) \to A ∖ \{y\} \in Fin$
27	24 25 26	sylancl	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to A ∖ \{y\} \in Fin$
28	3	adantr	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to F : A ⟶ B$
29		fssres	$⊢ (F : A ⟶ B \land A ∖ \{y\} \subseteq A) \to ({F ↾}_{(A ∖ \{y\})}) : A ∖ \{y\} ⟶ B$
30	28 25 29	sylancl	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to ({F ↾}_{(A ∖ \{y\})}) : A ∖ \{y\} ⟶ B$
31	1	adantr	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to F : A \underset{onto}{⟶} B$
32		foelrn	$⊢ (F : A \underset{onto}{⟶} B \land z \in B) \to \exists u \in A z = F (u)$
33	31 32	sylan	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land z \in B) \to \exists u \in A z = F (u)$
34		simprll	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to x \in A$
35		simprrr	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to x \neq y$
36		eldifsn	$⊢ x \in (A ∖ \{y\}) \leftrightarrow (x \in A \land x \neq y)$
37	34 35 36	sylanbrc	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to x \in (A ∖ \{y\})$
38		simprrl	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to F (x) = F (y)$
39	38	eqcomd	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to F (y) = F (x)$
40		fveq2	$⊢ w = x \to F (w) = F (x)$
41	40	rspceeqv	$⊢ (x \in (A ∖ \{y\}) \land F (y) = F (x)) \to \exists w \in (A ∖ \{y\}) F (y) = F (w)$
42	37 39 41	syl2anc	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to \exists w \in (A ∖ \{y\}) F (y) = F (w)$
43		fveqeq2	$⊢ u = y \to (F (u) = F (w) \leftrightarrow F (y) = F (w))$
44	43	rexbidv	$⊢ u = y \to (\exists w \in (A ∖ \{y\}) F (u) = F (w) \leftrightarrow \exists w \in (A ∖ \{y\}) F (y) = F (w))$
45	42 44	syl5ibrcom	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to (u = y \to \exists w \in (A ∖ \{y\}) F (u) = F (w))$
46	45	adantr	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land u \in A) \to (u = y \to \exists w \in (A ∖ \{y\}) F (u) = F (w))$
47	46	imp	$⊢ ((((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land u \in A) \land u = y) \to \exists w \in (A ∖ \{y\}) F (u) = F (w)$
48		eldifsn	$⊢ u \in (A ∖ \{y\}) \leftrightarrow (u \in A \land u \neq y)$
49		eqid	$⊢ F (u) = F (u)$
50		fveq2	$⊢ w = u \to F (w) = F (u)$
51	50	rspceeqv	$⊢ (u \in (A ∖ \{y\}) \land F (u) = F (u)) \to \exists w \in (A ∖ \{y\}) F (u) = F (w)$
52	49 51	mpan2	$⊢ u \in (A ∖ \{y\}) \to \exists w \in (A ∖ \{y\}) F (u) = F (w)$
53	48 52	sylbir	$⊢ (u \in A \land u \neq y) \to \exists w \in (A ∖ \{y\}) F (u) = F (w)$
54	53	adantll	$⊢ ((((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land u \in A) \land u \neq y) \to \exists w \in (A ∖ \{y\}) F (u) = F (w)$
55	47 54	pm2.61dane	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land u \in A) \to \exists w \in (A ∖ \{y\}) F (u) = F (w)$
56		fvres	$⊢ w \in (A ∖ \{y\}) \to ({F ↾}_{(A ∖ \{y\})}) (w) = F (w)$
57	56	eqeq2d	$⊢ w \in (A ∖ \{y\}) \to (z = ({F ↾}_{(A ∖ \{y\})}) (w) \leftrightarrow z = F (w))$
58	57	rexbiia	$⊢ \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w) \leftrightarrow \exists w \in (A ∖ \{y\}) z = F (w)$
59		eqeq1	$⊢ z = F (u) \to (z = F (w) \leftrightarrow F (u) = F (w))$
60	59	rexbidv	$⊢ z = F (u) \to (\exists w \in (A ∖ \{y\}) z = F (w) \leftrightarrow \exists w \in (A ∖ \{y\}) F (u) = F (w))$
61	58 60	bitrid	$⊢ z = F (u) \to (\exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w) \leftrightarrow \exists w \in (A ∖ \{y\}) F (u) = F (w))$
62	55 61	syl5ibrcom	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land u \in A) \to (z = F (u) \to \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w))$
63	62	rexlimdva	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to (\exists u \in A z = F (u) \to \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w))$
64	63	imp	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land \exists u \in A z = F (u)) \to \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w)$
65	33 64	syldan	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \land z \in B) \to \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w)$
66	65	ralrimiva	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to \forall z \in B \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w)$
67		dffo3	$⊢ ({F ↾}_{(A ∖ \{y\})}) : A ∖ \{y\} \underset{onto}{⟶} B \leftrightarrow (({F ↾}_{(A ∖ \{y\})}) : A ∖ \{y\} ⟶ B \land \forall z \in B \exists w \in (A ∖ \{y\}) z = ({F ↾}_{(A ∖ \{y\})}) (w))$
68	30 66 67	sylanbrc	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to ({F ↾}_{(A ∖ \{y\})}) : A ∖ \{y\} \underset{onto}{⟶} B$
69		fodomfi	$⊢ (A ∖ \{y\} \in Fin \land ({F ↾}_{(A ∖ \{y\})}) : A ∖ \{y\} \underset{onto}{⟶} B) \to B ≼ (A ∖ \{y\})$
70	27 68 69	syl2anc	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land ((x \in A \land y \in A) \land (F (x) = F (y) \land x \neq y))) \to B ≼ (A ∖ \{y\})$
71	70	anassrs	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to B ≼ (A ∖ \{y\})$
72	71	expr	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to (x \neq y \to B ≼ (A ∖ \{y\}))$
73	72	necon1bd	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to (\neg B ≼ (A ∖ \{y\}) \to x = y)$
74	23 73	mpd	$⊢ (((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \land F (x) = F (y)) \to x = y$
75	74	ex	$⊢ ((F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \land (x \in A \land y \in A)) \to (F (x) = F (y) \to x = y)$
76	75	ralrimivva	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)$
77		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
78	3 76 77	sylanbrc	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to F : A \underset{1-1}{⟶} B$
79		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
80	78 1 79	sylanbrc	$⊢ (F : A \underset{onto}{⟶} B \land A \approx B \land B \in Fin) \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem fofinf1o

Proof