| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pltval | Structured version Visualization version GIF version | ||
| Description: Less-than relation. (df-pss 3927 analog.) (Contributed by NM, 12-Oct-2011.) |
| Ref | Expression |
|---|---|
| pltval.l | ⊢ ≤ = (le‘𝐾) |
| pltval.s | ⊢ < = (lt‘𝐾) |
| Ref | Expression |
|---|---|
| pltval | ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pltval.l | . . . . 5 ⊢ ≤ = (le‘𝐾) | |
| 2 | pltval.s | . . . . 5 ⊢ < = (lt‘𝐾) | |
| 3 | 1, 2 | pltfval 18375 | . . . 4 ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I )) |
| 4 | 3 | breqd 5116 | . . 3 ⊢ (𝐾 ∈ 𝐴 → (𝑋 < 𝑌 ↔ 𝑋( ≤ ∖ I )𝑌)) |
| 5 | brdif 5158 | . . . 4 ⊢ (𝑋( ≤ ∖ I )𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑋 I 𝑌)) | |
| 6 | ideqg 5828 | . . . . . . 7 ⊢ (𝑌 ∈ 𝐶 → (𝑋 I 𝑌 ↔ 𝑋 = 𝑌)) | |
| 7 | 6 | necon3bbid 2997 | . . . . . 6 ⊢ (𝑌 ∈ 𝐶 → (¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌)) |
| 8 | 7 | adantl 486 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌)) |
| 9 | 8 | anbi2d 641 | . . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → ((𝑋 ≤ 𝑌 ∧ ¬ 𝑋 I 𝑌) ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
| 10 | 5, 9 | bitrid 286 | . . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋( ≤ ∖ I )𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
| 11 | 4, 10 | sylan9bb 518 | . 2 ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶)) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
| 12 | 11 | 3impb 1130 | 1 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∖ cdif 3904 class class class wbr 5105 I cid 5546 ‘cfv 6525 lecple 17307 ltcplt 18354 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pr 5395 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-iota 6481 df-fun 6527 df-fv 6533 df-plt 18374 |
| This theorem is referenced by: pltle 18377 pltne 18378 pleval2i 18380 pltnle 18382 pltval3 18383 plttr 18386 latnlemlt 18518 latnle 18519 ipolt 18581 ogrpaddlt 20199 ogrpsublt 20203 ornglmullt 20941 orngrmullt 20942 orngmullt 20943 ofldlt1 20947 opltn0 39826 cvrval2 39910 cvrnbtwn2 39911 cvrnbtwn3 39912 cvrle 39914 cvrnbtwn4 39915 cvrne 39917 atlltn0 39942 hlrelat5N 40037 llnle 40154 lplnle 40176 llncvrlpln2 40193 lplncvrlvol2 40251 lhp2lt 40637 lautlt 40727 |
| Copyright terms: Public domain | W3C validator |