MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pmltpclem2 Structured version   Visualization version   GIF version

Theorem pmltpclem2 25484
Description: Lemma for pmltpc 25485. (Contributed by Mario Carneiro, 1-Jul-2014.)
Hypotheses
Ref Expression
pmltpc.1 (𝜑𝐹 ∈ (ℝ ↑pm ℝ))
pmltpc.2 (𝜑𝐴 ⊆ dom 𝐹)
pmltpc.3 (𝜑𝑈𝐴)
pmltpc.4 (𝜑𝑉𝐴)
pmltpc.5 (𝜑𝑊𝐴)
pmltpc.6 (𝜑𝑋𝐴)
pmltpc.7 (𝜑𝑈𝑉)
pmltpc.8 (𝜑𝑊𝑋)
pmltpc.9 (𝜑 → ¬ (𝐹𝑈) ≤ (𝐹𝑉))
pmltpc.10 (𝜑 → ¬ (𝐹𝑋) ≤ (𝐹𝑊))
Assertion
Ref Expression
pmltpclem2 (𝜑 → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
Distinct variable groups:   𝑎,𝑏,𝑐,𝐴   𝐹,𝑎,𝑏,𝑐   𝑉,𝑏,𝑐   𝑈,𝑎,𝑏,𝑐   𝑊,𝑎,𝑏,𝑐   𝑋,𝑏,𝑐
Allowed substitution hints:   𝜑(𝑎,𝑏,𝑐)   𝑉(𝑎)   𝑋(𝑎)

Proof of Theorem pmltpclem2
StepHypRef Expression
1 pmltpc.5 . . . . 5 (𝜑𝑊𝐴)
21ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → 𝑊𝐴)
3 pmltpc.3 . . . . 5 (𝜑𝑈𝐴)
43ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → 𝑈𝐴)
5 pmltpc.4 . . . . 5 (𝜑𝑉𝐴)
65ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → 𝑉𝐴)
7 simpr 484 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → 𝑊 < 𝑈)
8 pmltpc.1 . . . . . . . . 9 (𝜑𝐹 ∈ (ℝ ↑pm ℝ))
9 reex 11246 . . . . . . . . . 10 ℝ ∈ V
109, 9elpm2 8914 . . . . . . . . 9 (𝐹 ∈ (ℝ ↑pm ℝ) ↔ (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ℝ))
118, 10sylib 218 . . . . . . . 8 (𝜑 → (𝐹:dom 𝐹⟶ℝ ∧ dom 𝐹 ⊆ ℝ))
1211simprd 495 . . . . . . 7 (𝜑 → dom 𝐹 ⊆ ℝ)
13 pmltpc.2 . . . . . . . 8 (𝜑𝐴 ⊆ dom 𝐹)
1413, 3sseldd 3984 . . . . . . 7 (𝜑𝑈 ∈ dom 𝐹)
1512, 14sseldd 3984 . . . . . 6 (𝜑𝑈 ∈ ℝ)
1613, 5sseldd 3984 . . . . . . 7 (𝜑𝑉 ∈ dom 𝐹)
1712, 16sseldd 3984 . . . . . 6 (𝜑𝑉 ∈ ℝ)
18 pmltpc.7 . . . . . 6 (𝜑𝑈𝑉)
1911simpld 494 . . . . . . . . 9 (𝜑𝐹:dom 𝐹⟶ℝ)
2019, 16ffvelcdmd 7105 . . . . . . . 8 (𝜑 → (𝐹𝑉) ∈ ℝ)
21 pmltpc.9 . . . . . . . . 9 (𝜑 → ¬ (𝐹𝑈) ≤ (𝐹𝑉))
2219, 14ffvelcdmd 7105 . . . . . . . . . 10 (𝜑 → (𝐹𝑈) ∈ ℝ)
2320, 22ltnled 11408 . . . . . . . . 9 (𝜑 → ((𝐹𝑉) < (𝐹𝑈) ↔ ¬ (𝐹𝑈) ≤ (𝐹𝑉)))
2421, 23mpbird 257 . . . . . . . 8 (𝜑 → (𝐹𝑉) < (𝐹𝑈))
2520, 24gtned 11396 . . . . . . 7 (𝜑 → (𝐹𝑈) ≠ (𝐹𝑉))
26 fveq2 6906 . . . . . . . . 9 (𝑉 = 𝑈 → (𝐹𝑉) = (𝐹𝑈))
2726eqcomd 2743 . . . . . . . 8 (𝑉 = 𝑈 → (𝐹𝑈) = (𝐹𝑉))
2827necon3i 2973 . . . . . . 7 ((𝐹𝑈) ≠ (𝐹𝑉) → 𝑉𝑈)
2925, 28syl 17 . . . . . 6 (𝜑𝑉𝑈)
3015, 17, 18, 29leneltd 11415 . . . . 5 (𝜑𝑈 < 𝑉)
3130ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → 𝑈 < 𝑉)
32 simplr 769 . . . . . 6 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → (𝐹𝑊) < (𝐹𝑈))
3324ad2antrr 726 . . . . . 6 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → (𝐹𝑉) < (𝐹𝑈))
3432, 33jca 511 . . . . 5 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → ((𝐹𝑊) < (𝐹𝑈) ∧ (𝐹𝑉) < (𝐹𝑈)))
3534orcd 874 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → (((𝐹𝑊) < (𝐹𝑈) ∧ (𝐹𝑉) < (𝐹𝑈)) ∨ ((𝐹𝑈) < (𝐹𝑊) ∧ (𝐹𝑈) < (𝐹𝑉))))
362, 4, 6, 7, 31, 35pmltpclem1 25483 . . 3 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑊 < 𝑈) → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
373ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑈𝐴)
381ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑊𝐴)
39 pmltpc.6 . . . . 5 (𝜑𝑋𝐴)
4039ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑋𝐴)
4115ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑈 ∈ ℝ)
4213, 1sseldd 3984 . . . . . . 7 (𝜑𝑊 ∈ dom 𝐹)
4312, 42sseldd 3984 . . . . . 6 (𝜑𝑊 ∈ ℝ)
4443ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑊 ∈ ℝ)
45 simpr 484 . . . . 5 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑈𝑊)
4619, 42ffvelcdmd 7105 . . . . . . . 8 (𝜑 → (𝐹𝑊) ∈ ℝ)
4746ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → (𝐹𝑊) ∈ ℝ)
48 simplr 769 . . . . . . 7 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → (𝐹𝑊) < (𝐹𝑈))
4947, 48gtned 11396 . . . . . 6 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → (𝐹𝑈) ≠ (𝐹𝑊))
50 fveq2 6906 . . . . . . . 8 (𝑊 = 𝑈 → (𝐹𝑊) = (𝐹𝑈))
5150eqcomd 2743 . . . . . . 7 (𝑊 = 𝑈 → (𝐹𝑈) = (𝐹𝑊))
5251necon3i 2973 . . . . . 6 ((𝐹𝑈) ≠ (𝐹𝑊) → 𝑊𝑈)
5349, 52syl 17 . . . . 5 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑊𝑈)
5441, 44, 45, 53leneltd 11415 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑈 < 𝑊)
5513, 39sseldd 3984 . . . . . . 7 (𝜑𝑋 ∈ dom 𝐹)
5612, 55sseldd 3984 . . . . . 6 (𝜑𝑋 ∈ ℝ)
57 pmltpc.8 . . . . . 6 (𝜑𝑊𝑋)
58 pmltpc.10 . . . . . . . . 9 (𝜑 → ¬ (𝐹𝑋) ≤ (𝐹𝑊))
5919, 55ffvelcdmd 7105 . . . . . . . . . 10 (𝜑 → (𝐹𝑋) ∈ ℝ)
6046, 59ltnled 11408 . . . . . . . . 9 (𝜑 → ((𝐹𝑊) < (𝐹𝑋) ↔ ¬ (𝐹𝑋) ≤ (𝐹𝑊)))
6158, 60mpbird 257 . . . . . . . 8 (𝜑 → (𝐹𝑊) < (𝐹𝑋))
6246, 61gtned 11396 . . . . . . 7 (𝜑 → (𝐹𝑋) ≠ (𝐹𝑊))
63 fveq2 6906 . . . . . . . 8 (𝑋 = 𝑊 → (𝐹𝑋) = (𝐹𝑊))
6463necon3i 2973 . . . . . . 7 ((𝐹𝑋) ≠ (𝐹𝑊) → 𝑋𝑊)
6562, 64syl 17 . . . . . 6 (𝜑𝑋𝑊)
6643, 56, 57, 65leneltd 11415 . . . . 5 (𝜑𝑊 < 𝑋)
6766ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → 𝑊 < 𝑋)
6861ad2antrr 726 . . . . . 6 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → (𝐹𝑊) < (𝐹𝑋))
6948, 68jca 511 . . . . 5 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → ((𝐹𝑊) < (𝐹𝑈) ∧ (𝐹𝑊) < (𝐹𝑋)))
7069olcd 875 . . . 4 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → (((𝐹𝑈) < (𝐹𝑊) ∧ (𝐹𝑋) < (𝐹𝑊)) ∨ ((𝐹𝑊) < (𝐹𝑈) ∧ (𝐹𝑊) < (𝐹𝑋))))
7137, 38, 40, 54, 67, 70pmltpclem1 25483 . . 3 (((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) ∧ 𝑈𝑊) → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
7243adantr 480 . . 3 ((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) → 𝑊 ∈ ℝ)
7315adantr 480 . . 3 ((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) → 𝑈 ∈ ℝ)
7436, 71, 72, 73ltlecasei 11369 . 2 ((𝜑 ∧ (𝐹𝑊) < (𝐹𝑈)) → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
753ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → 𝑈𝐴)
765ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → 𝑉𝐴)
7739ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → 𝑋𝐴)
7830ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → 𝑈 < 𝑉)
79 simpr 484 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → 𝑉 < 𝑋)
8024ad2antrr 726 . . . . . 6 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → (𝐹𝑉) < (𝐹𝑈))
8120adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑉) ∈ ℝ)
8222adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑈) ∈ ℝ)
8359adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑋) ∈ ℝ)
8424adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑉) < (𝐹𝑈))
8546adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑊) ∈ ℝ)
86 simpr 484 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑈) ≤ (𝐹𝑊))
8761adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑊) < (𝐹𝑋))
8882, 85, 83, 86, 87lelttrd 11419 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑈) < (𝐹𝑋))
8981, 82, 83, 84, 88lttrd 11422 . . . . . . 7 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → (𝐹𝑉) < (𝐹𝑋))
9089adantr 480 . . . . . 6 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → (𝐹𝑉) < (𝐹𝑋))
9180, 90jca 511 . . . . 5 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → ((𝐹𝑉) < (𝐹𝑈) ∧ (𝐹𝑉) < (𝐹𝑋)))
9291olcd 875 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → (((𝐹𝑈) < (𝐹𝑉) ∧ (𝐹𝑋) < (𝐹𝑉)) ∨ ((𝐹𝑉) < (𝐹𝑈) ∧ (𝐹𝑉) < (𝐹𝑋))))
9375, 76, 77, 78, 79, 92pmltpclem1 25483 . . 3 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑉 < 𝑋) → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
941ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑊𝐴)
9539ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑋𝐴)
965ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑉𝐴)
9766ad2antrr 726 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑊 < 𝑋)
9856ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑋 ∈ ℝ)
9917ad2antrr 726 . . . . 5 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑉 ∈ ℝ)
100 simpr 484 . . . . 5 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑋𝑉)
10120ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → (𝐹𝑉) ∈ ℝ)
10289adantr 480 . . . . . . 7 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → (𝐹𝑉) < (𝐹𝑋))
103101, 102gtned 11396 . . . . . 6 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → (𝐹𝑋) ≠ (𝐹𝑉))
104 fveq2 6906 . . . . . . . 8 (𝑉 = 𝑋 → (𝐹𝑉) = (𝐹𝑋))
105104eqcomd 2743 . . . . . . 7 (𝑉 = 𝑋 → (𝐹𝑋) = (𝐹𝑉))
106105necon3i 2973 . . . . . 6 ((𝐹𝑋) ≠ (𝐹𝑉) → 𝑉𝑋)
107103, 106syl 17 . . . . 5 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑉𝑋)
10898, 99, 100, 107leneltd 11415 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → 𝑋 < 𝑉)
10961ad2antrr 726 . . . . . 6 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → (𝐹𝑊) < (𝐹𝑋))
110109, 102jca 511 . . . . 5 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → ((𝐹𝑊) < (𝐹𝑋) ∧ (𝐹𝑉) < (𝐹𝑋)))
111110orcd 874 . . . 4 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → (((𝐹𝑊) < (𝐹𝑋) ∧ (𝐹𝑉) < (𝐹𝑋)) ∨ ((𝐹𝑋) < (𝐹𝑊) ∧ (𝐹𝑋) < (𝐹𝑉))))
11294, 95, 96, 97, 108, 111pmltpclem1 25483 . . 3 (((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) ∧ 𝑋𝑉) → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
11317adantr 480 . . 3 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → 𝑉 ∈ ℝ)
11456adantr 480 . . 3 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → 𝑋 ∈ ℝ)
11593, 112, 113, 114ltlecasei 11369 . 2 ((𝜑 ∧ (𝐹𝑈) ≤ (𝐹𝑊)) → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
11674, 115, 46, 22ltlecasei 11369 1 (𝜑 → ∃𝑎𝐴𝑏𝐴𝑐𝐴 (𝑎 < 𝑏𝑏 < 𝑐 ∧ (((𝐹𝑎) < (𝐹𝑏) ∧ (𝐹𝑐) < (𝐹𝑏)) ∨ ((𝐹𝑏) < (𝐹𝑎) ∧ (𝐹𝑏) < (𝐹𝑐)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wrex 3070  wss 3951   class class class wbr 5143  dom cdm 5685  wf 6557  cfv 6561  (class class class)co 7431  pm cpm 8867  cr 11154   < clt 11295  cle 11296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301
This theorem is referenced by:  pmltpc  25485
  Copyright terms: Public domain W3C validator