pltnle - Metamath Proof Explorer

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

Theorem pltnle 18391

Description: "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.)

**Hypotheses**
Ref	Expression
pleval2.b	⊢ 𝐵 = (Base‘𝐾)
pleval2.l	⊢ ≤ = (le‘𝐾)
pleval2.s	⊢ < = (lt‘𝐾)

**Assertion**
Ref	Expression
pltnle	⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)

**Proof of Theorem pltnle**
Step	Hyp	Ref	Expression
1		pleval2.l	. . . 4 ⊢ ≤ = (le‘𝐾)
2		pleval2.s	. . . 4 ⊢ < = (lt‘𝐾)
3	1, 2	pltval 18385	. . 3 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
4		pleval2.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
5	4, 1	posasymb 18374	. . . . . . 7 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
6	5	biimpd 232	. . . . . 6 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌))
7	6	expdimp 457	. . . . 5 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑌 ≤ 𝑋 → 𝑋 = 𝑌))
8	7	necon3ad 2977	. . . 4 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 ≠ 𝑌 → ¬ 𝑌 ≤ 𝑋))
9	8	expimpd 458	. . 3 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌) → ¬ 𝑌 ≤ 𝑋))
10	3, 9	sylbid 243	. 2 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ¬ 𝑌 ≤ 𝑋))
11	10	imp 411	1 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 class class class wbr 5113 ‘cfv 6537 Basecbs 17268 lecple 17316 Posetcpo 18362 ltcplt 18363

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-iota 6493 df-fun 6539 df-fv 6545 df-proset 18349 df-poset 18368 df-plt 18383

This theorem is referenced by: pltnlt 18393 pltn2lp 18394 ncvr1 39935 cvrnle 39943 atlrelat1 39984 cvrat 40085

W3C validator