![]() |
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 3785 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 17274 | . . . 4 ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I )) |
4 | 3 | breqd 4854 | . . 3 ⊢ (𝐾 ∈ 𝐴 → (𝑋 < 𝑌 ↔ 𝑋( ≤ ∖ I )𝑌)) |
5 | brdif 4896 | . . . 4 ⊢ (𝑋( ≤ ∖ I )𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑋 I 𝑌)) | |
6 | ideqg 5477 | . . . . . . 7 ⊢ (𝑌 ∈ 𝐶 → (𝑋 I 𝑌 ↔ 𝑋 = 𝑌)) | |
7 | 6 | necon3bbid 3008 | . . . . . 6 ⊢ (𝑌 ∈ 𝐶 → (¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌)) |
8 | 7 | adantl 474 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌)) |
9 | 8 | anbi2d 623 | . . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → ((𝑋 ≤ 𝑌 ∧ ¬ 𝑋 I 𝑌) ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
10 | 5, 9 | syl5bb 275 | . . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋( ≤ ∖ I )𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
11 | 4, 10 | sylan9bb 506 | . 2 ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶)) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
12 | 11 | 3impb 1144 | 1 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ≠ wne 2971 ∖ cdif 3766 class class class wbr 4843 I cid 5219 ‘cfv 6101 lecple 16274 ltcplt 17256 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-iota 6064 df-fun 6103 df-fv 6109 df-plt 17273 |
This theorem is referenced by: pltle 17276 pltne 17277 pleval2i 17279 pltnle 17281 pltval3 17282 plttr 17285 latnlemlt 17399 latnle 17400 ipolt 17474 ogrpaddlt 30234 ogrpsublt 30238 ornglmullt 30323 orngrmullt 30324 orngmullt 30325 ofldlt1 30329 opltn0 35211 cvrval2 35295 cvrnbtwn2 35296 cvrnbtwn3 35297 cvrle 35299 cvrnbtwn4 35300 cvrne 35302 atlltn0 35327 hlrelat5N 35422 llnle 35539 lplnle 35561 llncvrlpln2 35578 lplncvrlvol2 35636 lhp2lt 36022 lautlt 36112 |
Copyright terms: Public domain | W3C validator |