pmltpclem2

	Ref	Expression
Hypotheses	pmltpc.1	$⊢ φ \to F \in (ℝ ↑_{𝑝𝑚} ℝ)$
	pmltpc.2	$⊢ φ \to A \subseteq dom F$
	pmltpc.3	$⊢ φ \to U \in A$
	pmltpc.4	$⊢ φ \to V \in A$
	pmltpc.5	$⊢ φ \to W \in A$
	pmltpc.6	$⊢ φ \to X \in A$
	pmltpc.7	$⊢ φ \to U \leq V$
	pmltpc.8	$⊢ φ \to W \leq X$
	pmltpc.9	$⊢ φ \to \neg F (U) \leq F (V)$
	pmltpc.10	$⊢ φ \to \neg F (X) \leq F (W)$
Assertion	pmltpclem2	$⊢ φ \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$

Proof

Step	Hyp	Ref	Expression
1		pmltpc.1	$⊢ φ \to F \in (ℝ ↑_{𝑝𝑚} ℝ)$
2		pmltpc.2	$⊢ φ \to A \subseteq dom F$
3		pmltpc.3	$⊢ φ \to U \in A$
4		pmltpc.4	$⊢ φ \to V \in A$
5		pmltpc.5	$⊢ φ \to W \in A$
6		pmltpc.6	$⊢ φ \to X \in A$
7		pmltpc.7	$⊢ φ \to U \leq V$
8		pmltpc.8	$⊢ φ \to W \leq X$
9		pmltpc.9	$⊢ φ \to \neg F (U) \leq F (V)$
10		pmltpc.10	$⊢ φ \to \neg F (X) \leq F (W)$
11	5	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to W \in A$
12	3	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to U \in A$
13	4	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to V \in A$
14		simpr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to W < U$
15		reex	$⊢ ℝ \in V$
16	15 15	elpm2	$⊢ F \in (ℝ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℝ \land dom F \subseteq ℝ)$
17	1 16	sylib	$⊢ φ \to (F : dom F ⟶ ℝ \land dom F \subseteq ℝ)$
18	17	simprd	$⊢ φ \to dom F \subseteq ℝ$
19	2 3	sseldd	$⊢ φ \to U \in dom F$
20	18 19	sseldd	$⊢ φ \to U \in ℝ$
21	2 4	sseldd	$⊢ φ \to V \in dom F$
22	18 21	sseldd	$⊢ φ \to V \in ℝ$
23	17	simpld	$⊢ φ \to F : dom F ⟶ ℝ$
24	23 21	ffvelrnd	$⊢ φ \to F (V) \in ℝ$
25	23 19	ffvelrnd	$⊢ φ \to F (U) \in ℝ$
26	24 25	ltnled	$⊢ φ \to (F (V) < F (U) \leftrightarrow \neg F (U) \leq F (V))$
27	9 26	mpbird	$⊢ φ \to F (V) < F (U)$
28	24 27	gtned	$⊢ φ \to F (U) \neq F (V)$
29		fveq2	$⊢ V = U \to F (V) = F (U)$
30	29	eqcomd	$⊢ V = U \to F (U) = F (V)$
31	30	necon3i	$⊢ F (U) \neq F (V) \to V \neq U$
32	28 31	syl	$⊢ φ \to V \neq U$
33	20 22 7 32	leneltd	$⊢ φ \to U < V$
34	33	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to U < V$
35		simplr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to F (W) < F (U)$
36	27	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to F (V) < F (U)$
37	35 36	jca	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to (F (W) < F (U) \land F (V) < F (U))$
38	37	orcd	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to ((F (W) < F (U) \land F (V) < F (U)) \lor (F (U) < F (W) \land F (U) < F (V)))$
39	11 12 13 14 34 38	pmltpclem1	$⊢ ((φ \land F (W) < F (U)) \land W < U) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
40	3	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to U \in A$
41	5	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to W \in A$
42	6	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to X \in A$
43	20	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to U \in ℝ$
44	2 5	sseldd	$⊢ φ \to W \in dom F$
45	18 44	sseldd	$⊢ φ \to W \in ℝ$
46	45	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to W \in ℝ$
47		simpr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to U \leq W$
48	23 44	ffvelrnd	$⊢ φ \to F (W) \in ℝ$
49	48	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to F (W) \in ℝ$
50		simplr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to F (W) < F (U)$
51	49 50	gtned	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to F (U) \neq F (W)$
52		fveq2	$⊢ W = U \to F (W) = F (U)$
53	52	eqcomd	$⊢ W = U \to F (U) = F (W)$
54	53	necon3i	$⊢ F (U) \neq F (W) \to W \neq U$
55	51 54	syl	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to W \neq U$
56	43 46 47 55	leneltd	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to U < W$
57	2 6	sseldd	$⊢ φ \to X \in dom F$
58	18 57	sseldd	$⊢ φ \to X \in ℝ$
59	23 57	ffvelrnd	$⊢ φ \to F (X) \in ℝ$
60	48 59	ltnled	$⊢ φ \to (F (W) < F (X) \leftrightarrow \neg F (X) \leq F (W))$
61	10 60	mpbird	$⊢ φ \to F (W) < F (X)$
62	48 61	gtned	$⊢ φ \to F (X) \neq F (W)$
63		fveq2	$⊢ X = W \to F (X) = F (W)$
64	63	necon3i	$⊢ F (X) \neq F (W) \to X \neq W$
65	62 64	syl	$⊢ φ \to X \neq W$
66	45 58 8 65	leneltd	$⊢ φ \to W < X$
67	66	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to W < X$
68	61	ad2antrr	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to F (W) < F (X)$
69	50 68	jca	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to (F (W) < F (U) \land F (W) < F (X))$
70	69	olcd	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to ((F (U) < F (W) \land F (X) < F (W)) \lor (F (W) < F (U) \land F (W) < F (X)))$
71	40 41 42 56 67 70	pmltpclem1	$⊢ ((φ \land F (W) < F (U)) \land U \leq W) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
72	45	adantr	$⊢ (φ \land F (W) < F (U)) \to W \in ℝ$
73	20	adantr	$⊢ (φ \land F (W) < F (U)) \to U \in ℝ$
74	39 71 72 73	ltlecasei	$⊢ (φ \land F (W) < F (U)) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
75	3	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to U \in A$
76	4	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to V \in A$
77	6	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to X \in A$
78	33	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to U < V$
79		simpr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to V < X$
80	27	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to F (V) < F (U)$
81	24	adantr	$⊢ (φ \land F (U) \leq F (W)) \to F (V) \in ℝ$
82	25	adantr	$⊢ (φ \land F (U) \leq F (W)) \to F (U) \in ℝ$
83	59	adantr	$⊢ (φ \land F (U) \leq F (W)) \to F (X) \in ℝ$
84	27	adantr	$⊢ (φ \land F (U) \leq F (W)) \to F (V) < F (U)$
85	48	adantr	$⊢ (φ \land F (U) \leq F (W)) \to F (W) \in ℝ$
86		simpr	$⊢ (φ \land F (U) \leq F (W)) \to F (U) \leq F (W)$
87	61	adantr	$⊢ (φ \land F (U) \leq F (W)) \to F (W) < F (X)$
88	82 85 83 86 87	lelttrd	$⊢ (φ \land F (U) \leq F (W)) \to F (U) < F (X)$
89	81 82 83 84 88	lttrd	$⊢ (φ \land F (U) \leq F (W)) \to F (V) < F (X)$
90	89	adantr	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to F (V) < F (X)$
91	80 90	jca	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to (F (V) < F (U) \land F (V) < F (X))$
92	91	olcd	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to ((F (U) < F (V) \land F (X) < F (V)) \lor (F (V) < F (U) \land F (V) < F (X)))$
93	75 76 77 78 79 92	pmltpclem1	$⊢ ((φ \land F (U) \leq F (W)) \land V < X) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
94	5	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to W \in A$
95	6	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to X \in A$
96	4	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to V \in A$
97	66	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to W < X$
98	58	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to X \in ℝ$
99	22	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to V \in ℝ$
100		simpr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to X \leq V$
101	24	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to F (V) \in ℝ$
102	89	adantr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to F (V) < F (X)$
103	101 102	gtned	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to F (X) \neq F (V)$
104		fveq2	$⊢ V = X \to F (V) = F (X)$
105	104	eqcomd	$⊢ V = X \to F (X) = F (V)$
106	105	necon3i	$⊢ F (X) \neq F (V) \to V \neq X$
107	103 106	syl	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to V \neq X$
108	98 99 100 107	leneltd	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to X < V$
109	61	ad2antrr	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to F (W) < F (X)$
110	109 102	jca	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to (F (W) < F (X) \land F (V) < F (X))$
111	110	orcd	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to ((F (W) < F (X) \land F (V) < F (X)) \lor (F (X) < F (W) \land F (X) < F (V)))$
112	94 95 96 97 108 111	pmltpclem1	$⊢ ((φ \land F (U) \leq F (W)) \land X \leq V) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
113	22	adantr	$⊢ (φ \land F (U) \leq F (W)) \to V \in ℝ$
114	58	adantr	$⊢ (φ \land F (U) \leq F (W)) \to X \in ℝ$
115	93 112 113 114	ltlecasei	$⊢ (φ \land F (U) \leq F (W)) \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$
116	74 115 48 25	ltlecasei	$⊢ φ \to \exists a \in A \exists b \in A \exists c \in A (a < b \land b < c \land ((F (a) < F (b) \land F (c) < F (b)) \lor (F (b) < F (a) \land F (b) < F (c))))$

Metamath Proof Explorer

Theorem pmltpclem2

Proof