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 27974

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 27949	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ¬ 𝐵 <s 𝐴))
6	3, 4, 5	sylc 66	. 2 ⊢ (𝜑 → ¬ 𝐵 <s 𝐴)
7		lenlts 27953	. . 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 2146 class class class wbr 5114 No csur 27841 <s clts 27842 ≤s cles 27945

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pr 5409

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-ord 6370 df-on 6371 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-fv 6551 df-1o 8462 df-2o 8463 df-no 27844 df-lts 27845 df-les 27946

This theorem is used by: ltlesnd 27976 lemulsd 28368 mulsge0d 28376 mulsuniflem 28379 ltmuls12ad 28413 ltonold 28491 oncutlt 28494 onnolt 28496 n0sge0 28568 uzsind 28635 halfcut 28688 bdaypw2n0bndlem 28693 bdayfinbndlem1 28697 elreno2 28725 1reno 28727

W3C validator