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) Avoid ax-pow . (Revised by BTernaryTau, 26-Nov-2024)

		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		bren	$⊢ A \approx x \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} x$
3		pssss	$⊢ B \subset A \to B \subseteq A$
4		imass2	$⊢ B \subseteq A \to f [B] \subseteq f [A]$
5	3 4	syl	$⊢ B \subset A \to f [B] \subseteq f [A]$
6	5	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to f [B] \subseteq f [A]$
7		pssnel	$⊢ B \subset A \to \exists y (y \in A \land \neg y \in B)$
8		eldif	$⊢ y \in (A ∖ B) \leftrightarrow (y \in A \land \neg y \in B)$
9		f1ofn	$⊢ f : A \underset{1-1 onto}{⟶} x \to f Fn A$
10		difss	$⊢ A ∖ B \subseteq A$
11		fnfvima	$⊢ (f Fn A \land A ∖ B \subseteq A \land y \in (A ∖ B)) \to f (y) \in f [A ∖ B]$
12	11	3expia	$⊢ (f Fn A \land A ∖ B \subseteq A) \to (y \in (A ∖ B) \to f (y) \in f [A ∖ B])$
13	9 10 12	sylancl	$⊢ f : A \underset{1-1 onto}{⟶} x \to (y \in (A ∖ B) \to f (y) \in f [A ∖ B])$
14		dff1o3	$⊢ f : A \underset{1-1 onto}{⟶} x \leftrightarrow (f : A \underset{onto}{⟶} x \land Fun f^{-1})$
15		imadif	$⊢ Fun f^{-1} \to f [A ∖ B] = f [A] ∖ f [B]$
16	14 15	simplbiim	$⊢ f : A \underset{1-1 onto}{⟶} x \to f [A ∖ B] = f [A] ∖ f [B]$
17	16	eleq2d	$⊢ f : A \underset{1-1 onto}{⟶} x \to (f (y) \in f [A ∖ B] \leftrightarrow f (y) \in (f [A] ∖ f [B]))$
18	13 17	sylibd	$⊢ f : A \underset{1-1 onto}{⟶} x \to (y \in (A ∖ B) \to f (y) \in (f [A] ∖ f [B]))$
19		n0i	$⊢ f (y) \in (f [A] ∖ f [B]) \to \neg f [A] ∖ f [B] = \emptyset$
20	18 19	syl6	$⊢ f : A \underset{1-1 onto}{⟶} x \to (y \in (A ∖ B) \to \neg f [A] ∖ f [B] = \emptyset)$
21	8 20	biimtrrid	$⊢ f : A \underset{1-1 onto}{⟶} x \to ((y \in A \land \neg y \in B) \to \neg f [A] ∖ f [B] = \emptyset)$
22	21	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)$
23	22	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$
24	7 23	sylan2	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to \neg f [A] ∖ f [B] = \emptyset$
25		ssdif0	$⊢ f [A] \subseteq f [B] \leftrightarrow f [A] ∖ f [B] = \emptyset$
26	24 25	sylnibr	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to \neg f [A] \subseteq f [B]$
27		dfpss3	$⊢ f [B] \subset f [A] \leftrightarrow (f [B] \subseteq f [A] \land \neg f [A] \subseteq f [B])$
28	6 26 27	sylanbrc	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to f [B] \subset f [A]$
29		imadmrn	$⊢ f [dom f] = ran f$
30		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} x \to dom f = A$
31	30	imaeq2d	$⊢ f : A \underset{1-1 onto}{⟶} x \to f [dom f] = f [A]$
32		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} x \to f : A \underset{onto}{⟶} x$
33		forn	$⊢ f : A \underset{onto}{⟶} x \to ran f = x$
34	32 33	syl	$⊢ f : A \underset{1-1 onto}{⟶} x \to ran f = x$
35	29 31 34	3eqtr3a	$⊢ f : A \underset{1-1 onto}{⟶} x \to f [A] = x$
36	35	psseq2d	$⊢ f : A \underset{1-1 onto}{⟶} x \to (f [B] \subset f [A] \leftrightarrow f [B] \subset x)$
37	36	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to (f [B] \subset f [A] \leftrightarrow f [B] \subset x)$
38	28 37	mpbid	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to f [B] \subset x$
39		php2	$⊢ (x \in ω \land f [B] \subset x) \to f [B] ≺ x$
40	38 39	sylan2	$⊢ (x \in ω \land (f : A \underset{1-1 onto}{⟶} x \land B \subset A)) \to f [B] ≺ x$
41		nnfi	$⊢ x \in ω \to x \in Fin$
42		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} x \to f : A \underset{1-1}{⟶} x$
43		f1ores	$⊢ (f : A \underset{1-1}{⟶} x \land B \subseteq A) \to ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B]$
44	42 3 43	syl2an	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B]$
45		vex	$⊢ f \in V$
46	45	resex	$⊢ {f ↾}_{B} \in V$
47		f1oeq1	$⊢ y = {f ↾}_{B} \to (y : B \underset{1-1 onto}{⟶} f [B] \leftrightarrow ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B])$
48	46 47	spcev	$⊢ ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B] \to \exists y y : B \underset{1-1 onto}{⟶} f [B]$
49		bren	$⊢ B \approx f [B] \leftrightarrow \exists y y : B \underset{1-1 onto}{⟶} f [B]$
50	48 49	sylibr	$⊢ ({f ↾}_{B}) : B \underset{1-1 onto}{⟶} f [B] \to B \approx f [B]$
51	44 50	syl	$⊢ (f : A \underset{1-1 onto}{⟶} x \land B \subset A) \to B \approx f [B]$
52		endom	$⊢ B \approx f [B] \to B ≼ f [B]$
53		sdomdom	$⊢ f [B] ≺ x \to f [B] ≼ x$
54		domfi	$⊢ (x \in Fin \land f [B] ≼ x) \to f [B] \in Fin$
55	53 54	sylan2	$⊢ (x \in Fin \land f [B] ≺ x) \to f [B] \in Fin$
56	55	3adant2	$⊢ (x \in Fin \land B ≼ f [B] \land f [B] ≺ x) \to f [B] \in Fin$
57		domfi	$⊢ (f [B] \in Fin \land B ≼ f [B]) \to B \in Fin$
58	57	3adant3	$⊢ (f [B] \in Fin \land B ≼ f [B] \land f [B] ≺ x) \to B \in Fin$
59		domsdomtrfi	$⊢ (B \in Fin \land B ≼ f [B] \land f [B] ≺ x) \to B ≺ x$
60	58 59	syld3an1	$⊢ (f [B] \in Fin \land B ≼ f [B] \land f [B] ≺ x) \to B ≺ x$
61	56 60	syld3an1	$⊢ (x \in Fin \land B ≼ f [B] \land f [B] ≺ x) \to B ≺ x$
62	52 61	syl3an2	$⊢ (x \in Fin \land B \approx f [B] \land f [B] ≺ x) \to B ≺ x$
63	62	3expia	$⊢ (x \in Fin \land B \approx f [B]) \to (f [B] ≺ x \to B ≺ x)$
64	41 51 63	syl2an	$⊢ (x \in ω \land (f : A \underset{1-1 onto}{⟶} x \land B \subset A)) \to (f [B] ≺ x \to B ≺ x)$
65	40 64	mpd	$⊢ (x \in ω \land (f : A \underset{1-1 onto}{⟶} x \land B \subset A)) \to B ≺ x$
66	65	exp32	$⊢ x \in ω \to (f : A \underset{1-1 onto}{⟶} x \to (B \subset A \to B ≺ x))$
67	66	exlimdv	$⊢ x \in ω \to (\exists f f : A \underset{1-1 onto}{⟶} x \to (B \subset A \to B ≺ x))$
68	2 67	biimtrid	$⊢ x \in ω \to (A \approx x \to (B \subset A \to B ≺ x))$
69		ensymfib	$⊢ x \in Fin \to (x \approx A \leftrightarrow A \approx x)$
70	69	adantr	$⊢ (x \in Fin \land B ≺ x) \to (x \approx A \leftrightarrow A \approx x)$
71	70	biimp3ar	$⊢ (x \in Fin \land B ≺ x \land A \approx x) \to x \approx A$
72		endom	$⊢ x \approx A \to x ≼ A$
73		sdomdom	$⊢ B ≺ x \to B ≼ x$
74		domfi	$⊢ (x \in Fin \land B ≼ x) \to B \in Fin$
75	73 74	sylan2	$⊢ (x \in Fin \land B ≺ x) \to B \in Fin$
76	75	3adant3	$⊢ (x \in Fin \land B ≺ x \land x ≼ A) \to B \in Fin$
77		sdomdomtrfi	$⊢ (B \in Fin \land B ≺ x \land x ≼ A) \to B ≺ A$
78	76 77	syld3an1	$⊢ (x \in Fin \land B ≺ x \land x ≼ A) \to B ≺ A$
79	72 78	syl3an3	$⊢ (x \in Fin \land B ≺ x \land x \approx A) \to B ≺ A$
80	71 79	syld3an3	$⊢ (x \in Fin \land B ≺ x \land A \approx x) \to B ≺ A$
81	41 80	syl3an1	$⊢ (x \in ω \land B ≺ x \land A \approx x) \to B ≺ A$
82	81	3com23	$⊢ (x \in ω \land A \approx x \land B ≺ x) \to B ≺ A$
83	82	3exp	$⊢ x \in ω \to (A \approx x \to (B ≺ x \to B ≺ A))$
84	68 83	syldd	$⊢ x \in ω \to (A \approx x \to (B \subset A \to B ≺ A))$
85	84	rexlimiv	$⊢ \exists x \in ω A \approx x \to (B \subset A \to B ≺ A)$
86	1 85	sylbi	$⊢ A \in Fin \to (B \subset A \to B ≺ A)$
87	86	imp	$⊢ (A \in Fin \land B \subset A) \to B ≺ A$

Metamath Proof Explorer

Theorem php3

Proof