Metamath Proof Explorer

Theorem onnolt

Description: If a surreal ordinal is less than a given surreal, then it is simpler. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion onnolt ⊢ A ∈ On s ∧ B ∈ No ∧ A < s B → bday ⁡ A ∈ bday ⁡ B

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B ∈ bday ⁡ A → B ∈ No
2 onno ⊢ A ∈ On s → A ∈ No
3 2 adantr ⊢ A ∈ On s ∧ B ∈ No → A ∈ No
4 3 adantr ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B ∈ bday ⁡ A → A ∈ No
5 bdayon ⊢ bday ⁡ A ∈ On
6 simpr ⊢ A ∈ On s ∧ B ∈ No → B ∈ No
7 oldbday ⊢ bday ⁡ A ∈ On ∧ B ∈ No → B ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ B ∈ bday ⁡ A
8 5 6 7 sylancr ⊢ A ∈ On s ∧ B ∈ No → B ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ B ∈ bday ⁡ A
9 onleft ⊢ A ∈ On s → Old ⁡ bday ⁡ A = L ⁡ A
10 9 eleq2d ⊢ A ∈ On s → B ∈ Old ⁡ bday ⁡ A ↔ B ∈ L ⁡ A
11 10 adantr ⊢ A ∈ On s ∧ B ∈ No → B ∈ Old ⁡ bday ⁡ A ↔ B ∈ L ⁡ A
12 8 11 bitr3d ⊢ A ∈ On s ∧ B ∈ No → bday ⁡ B ∈ bday ⁡ A ↔ B ∈ L ⁡ A
13 leftlt ⊢ B ∈ L ⁡ A → B < s A
14 12 13 biimtrdi ⊢ A ∈ On s ∧ B ∈ No → bday ⁡ B ∈ bday ⁡ A → B < s A
15 14 imp ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B ∈ bday ⁡ A → B < s A
16 1 4 15 ltlesd ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B ∈ bday ⁡ A → B ≤ s A
17 16 ex ⊢ A ∈ On s ∧ B ∈ No → bday ⁡ B ∈ bday ⁡ A → B ≤ s A
18 leftssold ⊢ L ⁡ B ⊆ Old ⁡ bday ⁡ B
19 fveq2 ⊢ bday ⁡ B = bday ⁡ A → Old ⁡ bday ⁡ B = Old ⁡ bday ⁡ A
20 19 3ad2ant3 ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → Old ⁡ bday ⁡ B = Old ⁡ bday ⁡ A
21 9 3ad2ant1 ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → Old ⁡ bday ⁡ A = L ⁡ A
22 20 21 eqtrd ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → Old ⁡ bday ⁡ B = L ⁡ A
23 18 22 sseqtrid ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → L ⁡ B ⊆ L ⁡ A
24 simp2 ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → B ∈ No
25 2 3ad2ant1 ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → A ∈ No
26 simp3 ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → bday ⁡ B = bday ⁡ A
27 leslss ⊢ B ∈ No ∧ A ∈ No ∧ bday ⁡ B = bday ⁡ A → B ≤ s A ↔ L ⁡ B ⊆ L ⁡ A
28 24 25 26 27 syl3anc ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → B ≤ s A ↔ L ⁡ B ⊆ L ⁡ A
29 23 28 mpbird ⊢ A ∈ On s ∧ B ∈ No ∧ bday ⁡ B = bday ⁡ A → B ≤ s A
30 29 3expia ⊢ A ∈ On s ∧ B ∈ No → bday ⁡ B = bday ⁡ A → B ≤ s A
31 17 30 jaod ⊢ A ∈ On s ∧ B ∈ No → bday ⁡ B ∈ bday ⁡ A ∨ bday ⁡ B = bday ⁡ A → B ≤ s A
32 bdayon ⊢ bday ⁡ B ∈ On
33 32 5 onsseli ⊢ bday ⁡ B ⊆ bday ⁡ A ↔ bday ⁡ B ∈ bday ⁡ A ∨ bday ⁡ B = bday ⁡ A
34 ontri1 ⊢ bday ⁡ B ∈ On ∧ bday ⁡ A ∈ On → bday ⁡ B ⊆ bday ⁡ A ↔ ¬ bday ⁡ A ∈ bday ⁡ B
35 32 5 34 mp2an ⊢ bday ⁡ B ⊆ bday ⁡ A ↔ ¬ bday ⁡ A ∈ bday ⁡ B
36 33 35 bitr3i ⊢ bday ⁡ B ∈ bday ⁡ A ∨ bday ⁡ B = bday ⁡ A ↔ ¬ bday ⁡ A ∈ bday ⁡ B
37 36 a1i ⊢ A ∈ On s ∧ B ∈ No → bday ⁡ B ∈ bday ⁡ A ∨ bday ⁡ B = bday ⁡ A ↔ ¬ bday ⁡ A ∈ bday ⁡ B
38 lenlts ⊢ B ∈ No ∧ A ∈ No → B ≤ s A ↔ ¬ A < s B
39 6 3 38 syl2anc ⊢ A ∈ On s ∧ B ∈ No → B ≤ s A ↔ ¬ A < s B
40 31 37 39 3imtr3d ⊢ A ∈ On s ∧ B ∈ No → ¬ bday ⁡ A ∈ bday ⁡ B → ¬ A < s B
41 40 con4d ⊢ A ∈ On s ∧ B ∈ No → A < s B → bday ⁡ A ∈ bday ⁡ B
42 41 3impia ⊢ A ∈ On s ∧ B ∈ No ∧ A < s B → bday ⁡ A ∈ bday ⁡ B