php3

Description: Corollary of Pigeonhole Principle. If A is finite and B is a proper subset of A , the B is strictly less numerous than A . Stronger version of Corollary 6C of Enderton p. 135. (Contributed by NM, 22-Aug-2008)

		Ref	Expression
	Assertion	php3	$⊢ (A \in Fin \land B \subset A) \to B ≺ A$

Proof

Step	Hyp	Ref	Expression
1		isfi	$⊢ A \in Fin \leftrightarrow \exists x \in ω A \approx x$
2		relen	$⊢ Rel \approx$
3	2	brrelex1i	$⊢ A \approx x \to A \in V$
4		pssss	$⊢ B \subset A \to B \subseteq A$
5		ssdomg	$⊢ A \in V \to (B \subseteq A \to B ≼ A)$
6	5	imp	$⊢ (A \in V \land B \subseteq A) \to B ≼ A$
7	3 4 6	syl2an	$⊢ (A \approx x \land B \subset A) \to B ≼ A$
8	7	adantll	$⊢ ((x \in ω \land A \approx x) \land B \subset A) \to B ≼ A$
9		bren	$⊢ A \approx x \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} x$
10		imass2	$⊢ B \subseteq A \to f [B] \subseteq f [A]$
11	4 10	syl	$⊢ B \subset A \to f [B] \subseteq f [A]$
12	11	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to f [B] \subseteq f [A]$
13		pssnel	$⊢ B \subset A \to \exists y (y \in A \land \neg y \in B)$
14		eldif	$⊢ y \in (A ∖ B) \leftrightarrow (y \in A \land \neg y \in B)$
15		f1ofn	$⊢ f : A \underset{1-1 onto}{⟶} x \to f Fn A$
16		difss	$⊢ A ∖ B \subseteq A$
17		fnfvima	$⊢ (f Fn A \land A ∖ B \subseteq A \land y \in (A ∖ B)) \to f (y) \in f [A ∖ B]$
18	17	3expia	$⊢ (f Fn A \land A ∖ B \subseteq A) \to (y \in (A ∖ B) \to f (y) \in f [A ∖ B])$
19	15 16 18	sylancl	$⊢ f : A \underset{1-1 onto}{⟶} x \to (y \in (A ∖ B) \to f (y) \in f [A ∖ B])$
20		dff1o3	$⊢ f : A \underset{1-1 onto}{⟶} x \leftrightarrow (f : A \underset{onto}{⟶} x \land Fun f^{-1})$
21		imadif	$⊢ Fun f^{-1} \to f [A ∖ B] = f [A] ∖ f [B]$
22	20 21	simplbiim	$⊢ f : A \underset{1-1 onto}{⟶} x \to f [A ∖ B] = f [A] ∖ f [B]$
23	22	eleq2d	$⊢ f : A \underset{1-1 onto}{⟶} x \to (f (y) \in f [A ∖ B] \leftrightarrow f (y) \in (f [A] ∖ f [B]))$
24	19 23	sylibd	$⊢ f : A \underset{1-1 onto}{⟶} x \to (y \in (A ∖ B) \to f (y) \in (f [A] ∖ f [B]))$
25		n0i	$⊢ f (y) \in (f [A] ∖ f [B]) \to \neg f [A] ∖ f [B] = \emptyset$
26	24 25	syl6	$⊢ f : A \underset{1-1 onto}{⟶} x \to (y \in (A ∖ B) \to \neg f [A] ∖ f [B] = \emptyset)$
27	14 26	syl5bir	$⊢ f : A \underset{1-1 onto}{⟶} x \to ((y \in A \land \neg y \in B) \to \neg f [A] ∖ f [B] = \emptyset)$
28	27	exlimdv	$⊢ f : A \underset{1-1 onto}{⟶} x \to (\exists y (y \in A \land \neg y \in B) \to \neg f [A] ∖ f [B] = \emptyset)$
29	28	imp	$⊢ (f : A \underset{1-1 onto}{⟶} x \land \exists y (y \in A \land \neg y \in B)) \to \neg f [A] ∖ f [B] = \emptyset$
30	13 29	sylan2	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to \neg f [A] ∖ f [B] = \emptyset$
31		ssdif0	$⊢ f [A] \subseteq f [B] \leftrightarrow f [A] ∖ f [B] = \emptyset$
32	30 31	sylnibr	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to \neg f [A] \subseteq f [B]$
33		dfpss3	$⊢ f [B] \subset f [A] \leftrightarrow (f [B] \subseteq f [A] \land \neg f [A] \subseteq f [B])$
34	12 32 33	sylanbrc	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to f [B] \subset f [A]$
35		imadmrn	$⊢ f [dom f] = ran f$
36		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} x \to dom f = A$
37	36	imaeq2d	$⊢ f : A \underset{1-1 onto}{⟶} x \to f [dom f] = f [A]$
38		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} x \to f : A \underset{onto}{⟶} x$
39		forn	$⊢ f : A \underset{onto}{⟶} x \to ran f = x$
40	38 39	syl	$⊢ f : A \underset{1-1 onto}{⟶} x \to ran f = x$
41	35 37 40	3eqtr3a	$⊢ f : A \underset{1-1 onto}{⟶} x \to f [A] = x$
42	41	psseq2d	$⊢ f : A \underset{1-1 onto}{⟶} x \to (f [B] \subset f [A] \leftrightarrow f [B] \subset x)$
43	42	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to (f [B] \subset f [A] \leftrightarrow f [B] \subset x)$
44	34 43	mpbid	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to f [B] \subset x$
45		php	$⊢ (x \in ω \land f [B] \subset x) \to \neg x \approx f [B]$
46	44 45	sylan2	$⊢ (x \in ω \land (f : A \underset{1-1 onto}{⟶} x \land B \subset A)) \to \neg x \approx f [B]$
47		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} x \to f : A \underset{1-1}{⟶} x$
48		f1ores	$⊢ (f : A \underset{1-1}{⟶} x \land B \subseteq A) \to ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B]$
49	47 4 48	syl2an	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B]$
50		vex	$⊢ f \in V$
51	50	resex	$⊢ {f ↾}_{B} \in V$
52		f1oeq1	$⊢ y = {f ↾}_{B} \to (y : B \underset{1-1 onto}{⟶} f [B] \leftrightarrow ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B])$
53	51 52	spcev	$⊢ ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B] \to \exists y y : B \underset{1-1 onto}{⟶} f [B]$
54		bren	$⊢ B \approx f [B] \leftrightarrow \exists y y : B \underset{1-1 onto}{⟶} f [B]$
55	53 54	sylibr	$⊢ ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B] \to B \approx f [B]$
56	49 55	syl	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to B \approx f [B]$
57		entr	$⊢ (x \approx B \land B \approx f [B]) \to x \approx f [B]$
58	57	expcom	$⊢ B \approx f [B] \to (x \approx B \to x \approx f [B])$
59	56 58	syl	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to (x \approx B \to x \approx f [B])$
60	59	adantl	$⊢ (x \in ω \land (f : A \underset{1-1 onto}{⟶} x \land B \subset A)) \to (x \approx B \to x \approx f [B])$
61	46 60	mtod	$⊢ (x \in ω \land (f : A \underset{1-1 onto}{⟶} x \land B \subset A)) \to \neg x \approx B$
62	61	exp32	$⊢ x \in ω \to (f : A \underset{1-1 onto}{⟶} x \to (B \subset A \to \neg x \approx B))$
63	62	exlimdv	$⊢ x \in ω \to (\exists f f : A \underset{1-1 onto}{⟶} x \to (B \subset A \to \neg x \approx B))$
64	9 63	syl5bi	$⊢ x \in ω \to (A \approx x \to (B \subset A \to \neg x \approx B))$
65	64	imp31	$⊢ ((x \in ω \land A \approx x) \land B \subset A) \to \neg x \approx B$
66		entr	$⊢ (B \approx A \land A \approx x) \to B \approx x$
67	66	ex	$⊢ B \approx A \to (A \approx x \to B \approx x)$
68		ensym	$⊢ B \approx x \to x \approx B$
69	67 68	syl6com	$⊢ A \approx x \to (B \approx A \to x \approx B)$
70	69	ad2antlr	$⊢ ((x \in ω \land A \approx x) \land B \subset A) \to (B \approx A \to x \approx B)$
71	65 70	mtod	$⊢ ((x \in ω \land A \approx x) \land B \subset A) \to \neg B \approx A$
72		brsdom	$⊢ B ≺ A \leftrightarrow (B ≼ A \land \neg B \approx A)$
73	8 71 72	sylanbrc	$⊢ ((x \in ω \land A \approx x) \land B \subset A) \to B ≺ A$
74	73	exp31	$⊢ x \in ω \to (A \approx x \to (B \subset A \to B ≺ A))$
75	74	rexlimiv	$⊢ \exists x \in ω A \approx x \to (B \subset A \to B ≺ A)$
76	1 75	sylbi	$⊢ A \in Fin \to (B \subset A \to B ≺ A)$
77	76	imp	$⊢ (A \in Fin \land B \subset A) \to B ≺ A$

Metamath Proof Explorer

Theorem php3

Proof