Metamath Proof Explorer


Theorem sltlend

Description: Surreal less-than in terms of less-than or equal. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Hypotheses sltlen.1 âŠĒ ( 𝜑 → ðī ∈ No )
sltlen.2 âŠĒ ( 𝜑 → ðĩ ∈ No )
Assertion sltlend ( 𝜑 → ( ðī <s ðĩ ↔ ( ðī â‰Īs ðĩ ∧ ðĩ ≠ ðī ) ) )

Proof

Step Hyp Ref Expression
1 sltlen.1 âŠĒ ( 𝜑 → ðī ∈ No )
2 sltlen.2 âŠĒ ( 𝜑 → ðĩ ∈ No )
3 1 adantr âŠĒ ( ( 𝜑 ∧ ðī <s ðĩ ) → ðī ∈ No )
4 2 adantr âŠĒ ( ( 𝜑 ∧ ðī <s ðĩ ) → ðĩ ∈ No )
5 simpr âŠĒ ( ( 𝜑 ∧ ðī <s ðĩ ) → ðī <s ðĩ )
6 3 4 5 sltled âŠĒ ( ( 𝜑 ∧ ðī <s ðĩ ) → ðī â‰Īs ðĩ )
7 6 ex âŠĒ ( 𝜑 → ( ðī <s ðĩ → ðī â‰Īs ðĩ ) )
8 sltne âŠĒ ( ( ðī ∈ No ∧ ðī <s ðĩ ) → ðĩ ≠ ðī )
9 1 8 sylan âŠĒ ( ( 𝜑 ∧ ðī <s ðĩ ) → ðĩ ≠ ðī )
10 9 ex âŠĒ ( 𝜑 → ( ðī <s ðĩ → ðĩ ≠ ðī ) )
11 7 10 jcad âŠĒ ( 𝜑 → ( ðī <s ðĩ → ( ðī â‰Īs ðĩ ∧ ðĩ ≠ ðī ) ) )
12 sleloe âŠĒ ( ( ðī ∈ No ∧ ðĩ ∈ No ) → ( ðī â‰Īs ðĩ ↔ ( ðī <s ðĩ âˆĻ ðī = ðĩ ) ) )
13 1 2 12 syl2anc âŠĒ ( 𝜑 → ( ðī â‰Īs ðĩ ↔ ( ðī <s ðĩ âˆĻ ðī = ðĩ ) ) )
14 eqneqall âŠĒ ( ðĩ = ðī → ( ðĩ ≠ ðī → ðī <s ðĩ ) )
15 14 eqcoms âŠĒ ( ðī = ðĩ → ( ðĩ ≠ ðī → ðī <s ðĩ ) )
16 15 jao1i âŠĒ ( ( ðī <s ðĩ âˆĻ ðī = ðĩ ) → ( ðĩ ≠ ðī → ðī <s ðĩ ) )
17 13 16 biimtrdi âŠĒ ( 𝜑 → ( ðī â‰Īs ðĩ → ( ðĩ ≠ ðī → ðī <s ðĩ ) ) )
18 17 impd âŠĒ ( 𝜑 → ( ( ðī â‰Īs ðĩ ∧ ðĩ ≠ ðī ) → ðī <s ðĩ ) )
19 11 18 impbid âŠĒ ( 𝜑 → ( ðī <s ðĩ ↔ ( ðī â‰Īs ðĩ ∧ ðĩ ≠ ðī ) ) )