ltlesd - Metamath Proof Explorer

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

Theorem ltlesd 28017

Description: Surreal less-than implies less-than or equal. (Contributed by Scott Fenton, 16-Feb-2025.)

**Hypotheses**
Ref	Expression
ltlesd.1	⊢ (𝜑 → 𝐴 ∈ No )
ltlesd.2	⊢ (𝜑 → 𝐵 ∈ No )
ltlesd.3	⊢ (𝜑 → 𝐴 <s 𝐵)

**Assertion**
Ref	Expression
ltlesd	⊢ (𝜑 → 𝐴 ≤s 𝐵)

**Proof of Theorem ltlesd**
Step	Hyp	Ref	Expression
1		ltlesd.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ No )
2		ltlesd.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ No )
3	1, 2	jca 521	. . 3 ⊢ (𝜑 → (𝐴 ∈ No ∧ 𝐵 ∈ No ))
4		ltlesd.3	. . 3 ⊢ (𝜑 → 𝐴 <s 𝐵)
5		ltsasym 27992	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ¬ 𝐵 <s 𝐴))
6	3, 4, 5	sylc 66	. 2 ⊢ (𝜑 → ¬ 𝐵 <s 𝐴)
7		lenlts 27996	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
8	1, 2, 7	syl2anc 596	. 2 ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
9	6, 8	mpbird 260	1 ⊢ (𝜑 → 𝐴 ≤s 𝐵)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∈ wcel 2145 class class class wbr 5107 No csur 27884 <s clts 27885 ≤s cles 27988

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pr 5402

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-ord 6364 df-on 6365 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-1o 8459 df-2o 8460 df-no 27887 df-lts 27888 df-les 27989

This theorem is used by: ltlesnd 28019 lemulsd 28411 mulsge0d 28419 mulsuniflem 28422 ltmuls12ad 28456 ltonold 28534 oncutlt 28537 onnolt 28539 n0sge0 28611 uzsind 28678 halfcut 28731 bdaypw2n0bndlem 28736 bdayfinbndlem1 28740 elreno2 28768 1reno 28770

W3C validator