Theorem fphpd

Description: Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	fphpd.a	$$⊢\phi \to B\prec A$$
	fphpd.b	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	fphpd.c	$$⊢x=y\to C=D$$
Assertion	fphpd	$$⊢\phi \to \exists x\in A\exists y\in A\left(x\ne y\wedge C=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		fphpd.a	$$⊢\phi \to B\prec A$$
2		fphpd.b	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
3		fphpd.c	$$⊢x=y\to C=D$$
4		domnsym	$$⊢A\preccurlyeq B\to \neg B\prec A$$
5	4 1	nsyl3	$$⊢\phi \to \neg A\preccurlyeq B$$
6		relsdom	$$⊢\mathrm{Rel}\prec$$
7	6	brrelex1i	$$⊢B\prec A\to B\in \mathrm{V}$$
8	1 7	syl	$$⊢\phi \to B\in \mathrm{V}$$
9	8	adantr	$$⊢\left(\phi \wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)\to B\in \mathrm{V}$$
10		nfv	$$⊢Ⅎx\left(\phi \wedge a\in A\right)$$
11		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋a/x⦌C$$
12	11	nfel1	$$⊢Ⅎx⦋a/x⦌C\in B$$
13	10 12	nfim	$$⊢Ⅎx\left(\left(\phi \wedge a\in A\right)\to ⦋a/x⦌C\in B\right)$$
14		eleq1w	$$⊢x=a\to \left(x\in A\leftrightarrow a\in A\right)$$
15	14	anbi2d	$$⊢x=a\to \left(\left(\phi \wedge x\in A\right)\leftrightarrow \left(\phi \wedge a\in A\right)\right)$$
16		csbeq1a	$$⊢x=a\to C=⦋a/x⦌C$$
17	16	eleq1d	$$⊢x=a\to \left(C\in B\leftrightarrow ⦋a/x⦌C\in B\right)$$
18	15 17	imbi12d	$$⊢x=a\to \left(\left(\left(\phi \wedge x\in A\right)\to C\in B\right)\leftrightarrow \left(\left(\phi \wedge a\in A\right)\to ⦋a/x⦌C\in B\right)\right)$$
19	13 18 2	chvarfv	$$⊢\left(\phi \wedge a\in A\right)\to ⦋a/x⦌C\in B$$
20	19	ex	$$⊢\phi \to \left(a\in A\to ⦋a/x⦌C\in B\right)$$
21	20	adantr	$$⊢\left(\phi \wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)\to \left(a\in A\to ⦋a/x⦌C\in B\right)$$
22		csbid	$$⊢⦋x/x⦌C=C$$
23		vex	$$⊢y\in \mathrm{V}$$
24	23 3	csbie	$$⊢⦋y/x⦌C=D$$
25	22 24	eqeq12i	$$⊢⦋x/x⦌C=⦋y/x⦌C\leftrightarrow C=D$$
26	25	imbi1i	$$⊢\left(⦋x/x⦌C=⦋y/x⦌C\to x=y\right)\leftrightarrow \left(C=D\to x=y\right)$$
27	26	2ralbii	$$⊢\forall x\in A\forall y\in A\left(⦋x/x⦌C=⦋y/x⦌C\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\left(C=D\to x=y\right)$$
28		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
29	11 28	nfeq	$$⊢Ⅎx⦋a/x⦌C=⦋y/x⦌C$$
30		nfv	$$⊢Ⅎxa=y$$
31	29 30	nfim	$$⊢Ⅎx\left(⦋a/x⦌C=⦋y/x⦌C\to a=y\right)$$
32		nfv	$$⊢Ⅎy\left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)$$
33		csbeq1	$$⊢x=a\to ⦋x/x⦌C=⦋a/x⦌C$$
34	33	eqeq1d	$$⊢x=a\to \left(⦋x/x⦌C=⦋y/x⦌C\leftrightarrow ⦋a/x⦌C=⦋y/x⦌C\right)$$
35		equequ1	$$⊢x=a\to \left(x=y\leftrightarrow a=y\right)$$
36	34 35	imbi12d	$$⊢x=a\to \left(\left(⦋x/x⦌C=⦋y/x⦌C\to x=y\right)\leftrightarrow \left(⦋a/x⦌C=⦋y/x⦌C\to a=y\right)\right)$$
37		csbeq1	$$⊢y=b\to ⦋y/x⦌C=⦋b/x⦌C$$
38	37	eqeq2d	$$⊢y=b\to \left(⦋a/x⦌C=⦋y/x⦌C\leftrightarrow ⦋a/x⦌C=⦋b/x⦌C\right)$$
39		equequ2	$$⊢y=b\to \left(a=y\leftrightarrow a=b\right)$$
40	38 39	imbi12d	$$⊢y=b\to \left(\left(⦋a/x⦌C=⦋y/x⦌C\to a=y\right)\leftrightarrow \left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)\right)$$
41	31 32 36 40	rspc2	$$⊢\left(a\in A\wedge b\in A\right)\to \left(\forall x\in A\forall y\in A\left(⦋x/x⦌C=⦋y/x⦌C\to x=y\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)\right)$$
42	41	com12	$$⊢\forall x\in A\forall y\in A\left(⦋x/x⦌C=⦋y/x⦌C\to x=y\right)\to \left(\left(a\in A\wedge b\in A\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)\right)$$
43	27 42	sylbir	$$⊢\forall x\in A\forall y\in A\left(C=D\to x=y\right)\to \left(\left(a\in A\wedge b\in A\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)\right)$$
44		id	$$⊢\left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)$$
45		csbeq1	$$⊢a=b\to ⦋a/x⦌C=⦋b/x⦌C$$
46	44 45	impbid1	$$⊢\left(⦋a/x⦌C=⦋b/x⦌C\to a=b\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\leftrightarrow a=b\right)$$
47	43 46	syl6	$$⊢\forall x\in A\forall y\in A\left(C=D\to x=y\right)\to \left(\left(a\in A\wedge b\in A\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\leftrightarrow a=b\right)\right)$$
48	47	adantl	$$⊢\left(\phi \wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)\to \left(\left(a\in A\wedge b\in A\right)\to \left(⦋a/x⦌C=⦋b/x⦌C\leftrightarrow a=b\right)\right)$$
49	21 48	dom2d	$$⊢\left(\phi \wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)\to \left(B\in \mathrm{V}\to A\preccurlyeq B\right)$$
50	9 49	mpd	$$⊢\left(\phi \wedge \forall x\in A\forall y\in A\left(C=D\to x=y\right)\right)\to A\preccurlyeq B$$
51	5 50	mtand	$$⊢\phi \to \neg \forall x\in A\forall y\in A\left(C=D\to x=y\right)$$
52		ancom	$$⊢\left(\neg x=y\wedge C=D\right)\leftrightarrow \left(C=D\wedge \neg x=y\right)$$
53		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
54	53	anbi1i	$$⊢\left(x\ne y\wedge C=D\right)\leftrightarrow \left(\neg x=y\wedge C=D\right)$$
55		pm4.61	$$⊢\neg \left(C=D\to x=y\right)\leftrightarrow \left(C=D\wedge \neg x=y\right)$$
56	52 54 55	3bitr4i	$$⊢\left(x\ne y\wedge C=D\right)\leftrightarrow \neg \left(C=D\to x=y\right)$$
57	56	rexbii	$$⊢\exists y\in A\left(x\ne y\wedge C=D\right)\leftrightarrow \exists y\in A\neg \left(C=D\to x=y\right)$$
58		rexnal	$$⊢\exists y\in A\neg \left(C=D\to x=y\right)\leftrightarrow \neg \forall y\in A\left(C=D\to x=y\right)$$
59	57 58	bitri	$$⊢\exists y\in A\left(x\ne y\wedge C=D\right)\leftrightarrow \neg \forall y\in A\left(C=D\to x=y\right)$$
60	59	rexbii	$$⊢\exists x\in A\exists y\in A\left(x\ne y\wedge C=D\right)\leftrightarrow \exists x\in A\neg \forall y\in A\left(C=D\to x=y\right)$$
61		rexnal	$$⊢\exists x\in A\neg \forall y\in A\left(C=D\to x=y\right)\leftrightarrow \neg \forall x\in A\forall y\in A\left(C=D\to x=y\right)$$
62	60 61	bitri	$$⊢\exists x\in A\exists y\in A\left(x\ne y\wedge C=D\right)\leftrightarrow \neg \forall x\in A\forall y\in A\left(C=D\to x=y\right)$$
63	51 62	sylibr	$$⊢\phi \to \exists x\in A\exists y\in A\left(x\ne y\wedge C=D\right)$$