fphpdo

Description: Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014)

	Ref	Expression
Hypotheses	fphpdo.1	$⊢ φ \to A \subseteq ℝ$
	fphpdo.2	$⊢ φ \to B \in V$
	fphpdo.3	$⊢ φ \to B ≺ A$
	fphpdo.4	$⊢ (φ \land z \in A) \to C \in B$
	fphpdo.5	$⊢ z = x \to C = D$
	fphpdo.6	$⊢ z = y \to C = E$
Assertion	fphpdo	$⊢ φ \to \exists x \in A \exists y \in A (x < y \land D = E)$

Proof

Step	Hyp	Ref	Expression
1		fphpdo.1	$⊢ φ \to A \subseteq ℝ$
2		fphpdo.2	$⊢ φ \to B \in V$
3		fphpdo.3	$⊢ φ \to B ≺ A$
4		fphpdo.4	$⊢ (φ \land z \in A) \to C \in B$
5		fphpdo.5	$⊢ z = x \to C = D$
6		fphpdo.6	$⊢ z = y \to C = E$
7	4	fmpttd	$⊢ φ \to (z \in A ⟼ C) : A ⟶ B$
8	7	ffvelcdmda	$⊢ (φ \land b \in A) \to (z \in A ⟼ C) (b) \in B$
9		fveq2	$⊢ b = c \to (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)$
10	3 8 9	fphpd	$⊢ φ \to \exists b \in A \exists c \in A (b \neq c \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c))$
11	1	sselda	$⊢ (φ \land b \in A) \to b \in ℝ$
12	11	adantrr	$⊢ (φ \land (b \in A \land c \in A)) \to b \in ℝ$
13	12	adantr	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to b \in ℝ$
14	1	sselda	$⊢ (φ \land c \in A) \to c \in ℝ$
15	14	adantrl	$⊢ (φ \land (b \in A \land c \in A)) \to c \in ℝ$
16	15	adantr	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to c \in ℝ$
17	13 16	lttri2d	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to (b \neq c \leftrightarrow (b < c \lor c < b))$
18		simprl	$⊢ (φ \land (b \in A \land c \in A)) \to b \in A$
19	18	ad2antrr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land b < c) \to b \in A$
20		simprr	$⊢ (φ \land (b \in A \land c \in A)) \to c \in A$
21	20	ad2antrr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land b < c) \to c \in A$
22		simpr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land b < c) \to b < c$
23		simplr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land b < c) \to (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)$
24		breq1	$⊢ x = b \to (x < y \leftrightarrow b < y)$
25		fveqeq2	$⊢ x = b \to ((z \in A ⟼ C) (x) = (z \in A ⟼ C) (y) \leftrightarrow (z \in A ⟼ C) (b) = (z \in A ⟼ C) (y))$
26	24 25	anbi12d	$⊢ x = b \to ((x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)) \leftrightarrow (b < y \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (y)))$
27		breq2	$⊢ y = c \to (b < y \leftrightarrow b < c)$
28		fveq2	$⊢ y = c \to (z \in A ⟼ C) (y) = (z \in A ⟼ C) (c)$
29	28	eqeq2d	$⊢ y = c \to ((z \in A ⟼ C) (b) = (z \in A ⟼ C) (y) \leftrightarrow (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c))$
30	27 29	anbi12d	$⊢ y = c \to ((b < y \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (y)) \leftrightarrow (b < c \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)))$
31	26 30	rspc2ev	$⊢ (b \in A \land c \in A \land (b < c \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c))) \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y))$
32	19 21 22 23 31	syl112anc	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land b < c) \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y))$
33	32	ex	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to (b < c \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)))$
34	20	ad2antrr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land c < b) \to c \in A$
35	18	ad2antrr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land c < b) \to b \in A$
36		simpr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land c < b) \to c < b$
37		simplr	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land c < b) \to (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)$
38	37	eqcomd	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land c < b) \to (z \in A ⟼ C) (c) = (z \in A ⟼ C) (b)$
39		breq1	$⊢ x = c \to (x < y \leftrightarrow c < y)$
40		fveqeq2	$⊢ x = c \to ((z \in A ⟼ C) (x) = (z \in A ⟼ C) (y) \leftrightarrow (z \in A ⟼ C) (c) = (z \in A ⟼ C) (y))$
41	39 40	anbi12d	$⊢ x = c \to ((x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)) \leftrightarrow (c < y \land (z \in A ⟼ C) (c) = (z \in A ⟼ C) (y)))$
42		breq2	$⊢ y = b \to (c < y \leftrightarrow c < b)$
43		fveq2	$⊢ y = b \to (z \in A ⟼ C) (y) = (z \in A ⟼ C) (b)$
44	43	eqeq2d	$⊢ y = b \to ((z \in A ⟼ C) (c) = (z \in A ⟼ C) (y) \leftrightarrow (z \in A ⟼ C) (c) = (z \in A ⟼ C) (b))$
45	42 44	anbi12d	$⊢ y = b \to ((c < y \land (z \in A ⟼ C) (c) = (z \in A ⟼ C) (y)) \leftrightarrow (c < b \land (z \in A ⟼ C) (c) = (z \in A ⟼ C) (b)))$
46	41 45	rspc2ev	$⊢ (c \in A \land b \in A \land (c < b \land (z \in A ⟼ C) (c) = (z \in A ⟼ C) (b))) \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y))$
47	34 35 36 38 46	syl112anc	$⊢ (((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \land c < b) \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y))$
48	47	ex	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to (c < b \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)))$
49	33 48	jaod	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to ((b < c \lor c < b) \to \exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)))$
50		eqid	$⊢ (z \in A ⟼ C) = (z \in A ⟼ C)$
51		simplr	$⊢ ((φ \land x \in A) \land y \in A) \to x \in A$
52		eleq1w	$⊢ z = x \to (z \in A \leftrightarrow x \in A)$
53	52	anbi2d	$⊢ z = x \to ((φ \land z \in A) \leftrightarrow (φ \land x \in A))$
54	5	eleq1d	$⊢ z = x \to (C \in B \leftrightarrow D \in B)$
55	53 54	imbi12d	$⊢ z = x \to (((φ \land z \in A) \to C \in B) \leftrightarrow ((φ \land x \in A) \to D \in B))$
56	55 4	chvarvv	$⊢ (φ \land x \in A) \to D \in B$
57	56	adantr	$⊢ ((φ \land x \in A) \land y \in A) \to D \in B$
58	50 5 51 57	fvmptd3	$⊢ ((φ \land x \in A) \land y \in A) \to (z \in A ⟼ C) (x) = D$
59		simpr	$⊢ ((φ \land x \in A) \land y \in A) \to y \in A$
60		eleq1w	$⊢ z = y \to (z \in A \leftrightarrow y \in A)$
61	60	anbi2d	$⊢ z = y \to ((φ \land z \in A) \leftrightarrow (φ \land y \in A))$
62	6	eleq1d	$⊢ z = y \to (C \in B \leftrightarrow E \in B)$
63	61 62	imbi12d	$⊢ z = y \to (((φ \land z \in A) \to C \in B) \leftrightarrow ((φ \land y \in A) \to E \in B))$
64	63 4	chvarvv	$⊢ (φ \land y \in A) \to E \in B$
65	64	adantlr	$⊢ ((φ \land x \in A) \land y \in A) \to E \in B$
66	50 6 59 65	fvmptd3	$⊢ ((φ \land x \in A) \land y \in A) \to (z \in A ⟼ C) (y) = E$
67	58 66	eqeq12d	$⊢ ((φ \land x \in A) \land y \in A) \to ((z \in A ⟼ C) (x) = (z \in A ⟼ C) (y) \leftrightarrow D = E)$
68	67	biimpd	$⊢ ((φ \land x \in A) \land y \in A) \to ((z \in A ⟼ C) (x) = (z \in A ⟼ C) (y) \to D = E)$
69	68	anim2d	$⊢ ((φ \land x \in A) \land y \in A) \to ((x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)) \to (x < y \land D = E))$
70	69	reximdva	$⊢ (φ \land x \in A) \to (\exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)) \to \exists y \in A (x < y \land D = E))$
71	70	reximdva	$⊢ φ \to (\exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)) \to \exists x \in A \exists y \in A (x < y \land D = E))$
72	71	ad2antrr	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to (\exists x \in A \exists y \in A (x < y \land (z \in A ⟼ C) (x) = (z \in A ⟼ C) (y)) \to \exists x \in A \exists y \in A (x < y \land D = E))$
73	49 72	syld	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to ((b < c \lor c < b) \to \exists x \in A \exists y \in A (x < y \land D = E))$
74	17 73	sylbid	$⊢ ((φ \land (b \in A \land c \in A)) \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to (b \neq c \to \exists x \in A \exists y \in A (x < y \land D = E))$
75	74	expimpd	$⊢ (φ \land (b \in A \land c \in A)) \to (((z \in A ⟼ C) (b) = (z \in A ⟼ C) (c) \land b \neq c) \to \exists x \in A \exists y \in A (x < y \land D = E))$
76	75	ancomsd	$⊢ (φ \land (b \in A \land c \in A)) \to ((b \neq c \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to \exists x \in A \exists y \in A (x < y \land D = E))$
77	76	rexlimdvva	$⊢ φ \to (\exists b \in A \exists c \in A (b \neq c \land (z \in A ⟼ C) (b) = (z \in A ⟼ C) (c)) \to \exists x \in A \exists y \in A (x < y \land D = E))$
78	10 77	mpd	$⊢ φ \to \exists x \in A \exists y \in A (x < y \land D = E)$

Metamath Proof Explorer

Theorem fphpdo

Proof