Metamath Proof Explorer

Theorem onscutlt

Description: A surreal ordinal is the simplest number greater than all previous surreal ordinals. Theorem 15 of Conway p. 28. (Contributed by Scott Fenton, 4-Nov-2025)

Ref Expression
Assertion onscutlt ( 𝐴 ∈ Ons → 𝐴 = ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) )

Proof

Step Hyp Ref Expression
1 onsno ⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
2 sltonex ⊢ ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∈ V )
3 1 2 syl ⊢ ( 𝐴 ∈ Ons → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∈ V )
4 snexg ⊢ ( 𝐴 ∈ Ons → { 𝐴 } ∈ V )
5 ssrab2 ⊢ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ Ons
6 onssno ⊢ Ons ⊆ No
7 5 6 sstri ⊢ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ No
8 7 a1i ⊢ ( 𝐴 ∈ Ons → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ No )
9 1 snssd ⊢ ( 𝐴 ∈ Ons → { 𝐴 } ⊆ No )
10 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 <s 𝐴 ↔ 𝑦 <s 𝐴 ) )
11 10 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ↔ ( 𝑦 ∈ Ons ∧ 𝑦 <s 𝐴 ) )
12 11 simprbi ⊢ ( 𝑦 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } → 𝑦 <s 𝐴 )
13 velsn ⊢ ( 𝑧 ∈ { 𝐴 } ↔ 𝑧 = 𝐴 )
14 breq2 ⊢ ( 𝑧 = 𝐴 → ( 𝑦 <s 𝑧 ↔ 𝑦 <s 𝐴 ) )
15 13 14 sylbi ⊢ ( 𝑧 ∈ { 𝐴 } → ( 𝑦 <s 𝑧 ↔ 𝑦 <s 𝐴 ) )
16 12 15 syl5ibrcom ⊢ ( 𝑦 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } → ( 𝑧 ∈ { 𝐴 } → 𝑦 <s 𝑧 ) )
17 16 imp ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∧ 𝑧 ∈ { 𝐴 } ) → 𝑦 <s 𝑧 )
18 17 3adant1 ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∧ 𝑧 ∈ { 𝐴 } ) → 𝑦 <s 𝑧 )
19 3 4 8 9 18 ssltd ⊢ ( 𝐴 ∈ Ons → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝐴 } )
20 snelpwi ⊢ ( 𝐴 ∈ No → { 𝐴 } ∈ 𝒫 No )
21 nulssgt ⊢ ( { 𝐴 } ∈ 𝒫 No → { 𝐴 } <<s ∅ )
22 1 20 21 3syl ⊢ ( 𝐴 ∈ Ons → { 𝐴 } <<s ∅ )
23 ssltsep ⊢ ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } → ∀ 𝑧 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∀ 𝑤 ∈ { 𝑦 } 𝑧 <s 𝑤 )
24 vex ⊢ 𝑦 ∈ V
25 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑧 <s 𝑤 ↔ 𝑧 <s 𝑦 ) )
26 24 25 ralsn ⊢ ( ∀ 𝑤 ∈ { 𝑦 } 𝑧 <s 𝑤 ↔ 𝑧 <s 𝑦 )
27 26 ralbii ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∀ 𝑤 ∈ { 𝑦 } 𝑧 <s 𝑤 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } 𝑧 <s 𝑦 )
28 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 <s 𝐴 ↔ 𝑧 <s 𝐴 ) )
29 28 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } 𝑧 <s 𝑦 ↔ ∀ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 → 𝑧 <s 𝑦 ) )
30 27 29 bitri ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∀ 𝑤 ∈ { 𝑦 } 𝑧 <s 𝑤 ↔ ∀ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 → 𝑧 <s 𝑦 ) )
31 23 30 sylib ⊢ ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } → ∀ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 → 𝑧 <s 𝑦 ) )
32 fvex ⊢ ( L ‘ 𝑦 ) ∈ V
33 fvex ⊢ ( R ‘ 𝑦 ) ∈ V
34 32 33 unex ⊢ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∈ V
35 34 a1i ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∈ V )
36 leftssno ⊢ ( L ‘ 𝑦 ) ⊆ No
37 rightssno ⊢ ( R ‘ 𝑦 ) ⊆ No
38 36 37 unssi ⊢ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ⊆ No
39 38 a1i ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ⊆ No )
40 eqidd ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) )
41 35 39 40 elons2d ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ Ons )
42 34 elpw ⊢ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∈ 𝒫 No ↔ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ⊆ No )
43 38 42 mpbir ⊢ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∈ 𝒫 No
44 nulssgt ⊢ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∈ 𝒫 No → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) <<s ∅ )
45 43 44 mp1i ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) <<s ∅ )
46 un0 ⊢ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ ∅ ) = ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) )
47 lrold ⊢ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) = ( O ‘ ( bday ‘ 𝑦 ) )
48 46 47 eqtri ⊢ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ ∅ ) = ( O ‘ ( bday ‘ 𝑦 ) )
49 48 imaeq2i ⊢ ( bday “ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ ∅ ) ) = ( bday “ ( O ‘ ( bday ‘ 𝑦 ) ) )
50 simpr ⊢ ( ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ) → 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) )
51 bdayelon ⊢ ( bday ‘ 𝑦 ) ∈ On
52 oldssno ⊢ ( O ‘ ( bday ‘ 𝑦 ) ) ⊆ No
53 52 sseli ⊢ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) → 𝑧 ∈ No )
54 53 adantl ⊢ ( ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ) → 𝑧 ∈ No )
55 oldbday ⊢ ( ( ( bday ‘ 𝑦 ) ∈ On ∧ 𝑧 ∈ No ) → ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ↔ ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑦 ) ) )
56 51 54 55 sylancr ⊢ ( ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ) → ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ↔ ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑦 ) ) )
57 50 56 mpbid ⊢ ( ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ) → ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑦 ) )
58 57 ralrimiva ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ∀ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑦 ) )
59 bdayfun ⊢ Fun bday
60 bdaydm ⊢ dom bday = No
61 52 60 sseqtrri ⊢ ( O ‘ ( bday ‘ 𝑦 ) ) ⊆ dom bday
62 funimass4 ⊢ ( ( Fun bday ∧ ( O ‘ ( bday ‘ 𝑦 ) ) ⊆ dom bday ) → ( ( bday “ ( O ‘ ( bday ‘ 𝑦 ) ) ) ⊆ ( bday ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑦 ) ) )
63 59 61 62 mp2an ⊢ ( ( bday “ ( O ‘ ( bday ‘ 𝑦 ) ) ) ⊆ ( bday ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ( bday ‘ 𝑧 ) ∈ ( bday ‘ 𝑦 ) )
64 58 63 sylibr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday “ ( O ‘ ( bday ‘ 𝑦 ) ) ) ⊆ ( bday ‘ 𝑦 ) )
65 49 64 eqsstrid ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday “ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ ∅ ) ) ⊆ ( bday ‘ 𝑦 ) )
66 scutbdaybnd ⊢ ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) <<s ∅ ∧ ( bday ‘ 𝑦 ) ∈ On ∧ ( bday “ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ ∅ ) ) ⊆ ( bday ‘ 𝑦 ) ) → ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ⊆ ( bday ‘ 𝑦 ) )
67 51 66 mp3an2 ⊢ ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) <<s ∅ ∧ ( bday “ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ ∅ ) ) ⊆ ( bday ‘ 𝑦 ) ) → ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ⊆ ( bday ‘ 𝑦 ) )
68 45 65 67 syl2anc ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ⊆ ( bday ‘ 𝑦 ) )
69 simpr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) )
70 bdayelon ⊢ ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ On
71 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
72 ontr2 ⊢ ( ( ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ⊆ ( bday ‘ 𝑦 ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ ( bday ‘ 𝐴 ) ) )
73 70 71 72 mp2an ⊢ ( ( ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ⊆ ( bday ‘ 𝑦 ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ ( bday ‘ 𝐴 ) )
74 68 69 73 syl2anc ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ ( bday ‘ 𝐴 ) )
75 45 scutcld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ No )
76 oldbday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ No ) → ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ ( bday ‘ 𝐴 ) ) )
77 71 75 76 sylancr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ∈ ( bday ‘ 𝐴 ) ) )
78 74 77 mpbird ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
79 elons ⊢ ( 𝐴 ∈ Ons ↔ ( 𝐴 ∈ No ∧ ( R ‘ 𝐴 ) = ∅ ) )
80 79 simprbi ⊢ ( 𝐴 ∈ Ons → ( R ‘ 𝐴 ) = ∅ )
81 80 ad2antrr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( R ‘ 𝐴 ) = ∅ )
82 81 uneq2d ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( ( L ‘ 𝐴 ) ∪ ∅ ) )
83 lrold ⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) )
84 un0 ⊢ ( ( L ‘ 𝐴 ) ∪ ∅ ) = ( L ‘ 𝐴 )
85 82 83 84 3eqtr3g ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
86 78 85 eleqtrd ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ ( L ‘ 𝐴 ) )
87 leftlt ⊢ ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ ( L ‘ 𝐴 ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝐴 )
88 86 87 syl ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝐴 )
89 simplr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → 𝑦 ∈ No )
90 slerflex ⊢ ( 𝑦 ∈ No → 𝑦 ≤s 𝑦 )
91 lrcut ⊢ ( 𝑦 ∈ No → ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) = 𝑦 )
92 90 91 breqtrrd ⊢ ( 𝑦 ∈ No → 𝑦 ≤s ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) )
93 89 92 syl ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → 𝑦 ≤s ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) )
94 uneq2 ⊢ ( ( R ‘ 𝑦 ) = ∅ → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) = ( ( L ‘ 𝑦 ) ∪ ∅ ) )
95 un0 ⊢ ( ( L ‘ 𝑦 ) ∪ ∅ ) = ( L ‘ 𝑦 )
96 94 95 eqtrdi ⊢ ( ( R ‘ 𝑦 ) = ∅ → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) = ( L ‘ 𝑦 ) )
97 eqcom ⊢ ( ( R ‘ 𝑦 ) = ∅ ↔ ∅ = ( R ‘ 𝑦 ) )
98 97 biimpi ⊢ ( ( R ‘ 𝑦 ) = ∅ → ∅ = ( R ‘ 𝑦 ) )
99 96 98 oveq12d ⊢ ( ( R ‘ 𝑦 ) = ∅ → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) = ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) )
100 99 breq2d ⊢ ( ( R ‘ 𝑦 ) = ∅ → ( 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ↔ 𝑦 ≤s ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) ) )
101 93 100 imbitrrid ⊢ ( ( R ‘ 𝑦 ) = ∅ → ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) )
102 simprlr ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 ∈ No )
103 75 adantl ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ No )
104 n0 ⊢ ( ( R ‘ 𝑦 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( R ‘ 𝑦 ) )
105 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑦 ≤s 𝑧 ↔ 𝑦 ≤s 𝑤 ) )
106 elun2 ⊢ ( 𝑤 ∈ ( R ‘ 𝑦 ) → 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
107 106 adantr ⊢ ( ( 𝑤 ∈ ( R ‘ 𝑦 ) ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑤 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
108 simprlr ⊢ ( ( 𝑤 ∈ ( R ‘ 𝑦 ) ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 ∈ No )
109 37 sseli ⊢ ( 𝑤 ∈ ( R ‘ 𝑦 ) → 𝑤 ∈ No )
110 109 adantr ⊢ ( ( 𝑤 ∈ ( R ‘ 𝑦 ) ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑤 ∈ No )
111 rightgt ⊢ ( 𝑤 ∈ ( R ‘ 𝑦 ) → 𝑦 <s 𝑤 )
112 111 adantr ⊢ ( ( 𝑤 ∈ ( R ‘ 𝑦 ) ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 <s 𝑤 )
113 108 110 112 sltled ⊢ ( ( 𝑤 ∈ ( R ‘ 𝑦 ) ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 ≤s 𝑤 )
114 105 107 113 rspcedvdw ⊢ ( ( 𝑤 ∈ ( R ‘ 𝑦 ) ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 )
115 114 ex ⊢ ( 𝑤 ∈ ( R ‘ 𝑦 ) → ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 ) )
116 115 exlimiv ⊢ ( ∃ 𝑤 𝑤 ∈ ( R ‘ 𝑦 ) → ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 ) )
117 104 116 sylbi ⊢ ( ( R ‘ 𝑦 ) ≠ ∅ → ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 ) )
118 117 imp ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 )
119 118 orcd ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑦 ) 𝑤 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) )
120 lltropt ⊢ ( L ‘ 𝑦 ) <<s ( R ‘ 𝑦 )
121 120 a1i ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( L ‘ 𝑦 ) <<s ( R ‘ 𝑦 ) )
122 43 44 mp1i ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) <<s ∅ )
123 102 91 syl ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) = 𝑦 )
124 123 eqcomd ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 = ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) )
125 eqidd ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) )
126 sltrec ⊢ ( ( ( ( L ‘ 𝑦 ) <<s ( R ‘ 𝑦 ) ∧ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) <<s ∅ ) ∧ ( 𝑦 = ( ( L ‘ 𝑦 ) |s ( R ‘ 𝑦 ) ) ∧ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ) → ( 𝑦 <s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ↔ ( ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑦 ) 𝑤 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ) )
127 121 122 124 125 126 syl22anc ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → ( 𝑦 <s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ↔ ( ∃ 𝑧 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝑦 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑦 ) 𝑤 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) ) )
128 119 127 mpbird ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 <s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) )
129 102 103 128 sltled ⊢ ( ( ( R ‘ 𝑦 ) ≠ ∅ ∧ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) ) → 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) )
130 129 ex ⊢ ( ( R ‘ 𝑦 ) ≠ ∅ → ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ) )
131 101 130 pm2.61ine ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) )
132 slenlt ⊢ ( ( 𝑦 ∈ No ∧ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ No ) → ( 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ↔ ¬ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 ) )
133 89 75 132 syl2anc ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ( 𝑦 ≤s ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ↔ ¬ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 ) )
134 131 133 mpbid ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ¬ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 )
135 breq1 ⊢ ( 𝑧 = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) → ( 𝑧 <s 𝐴 ↔ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝐴 ) )
136 breq1 ⊢ ( 𝑧 = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) → ( 𝑧 <s 𝑦 ↔ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 ) )
137 136 notbid ⊢ ( 𝑧 = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) → ( ¬ 𝑧 <s 𝑦 ↔ ¬ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 ) )
138 135 137 anbi12d ⊢ ( 𝑧 = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) → ( ( 𝑧 <s 𝐴 ∧ ¬ 𝑧 <s 𝑦 ) ↔ ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝐴 ∧ ¬ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 ) ) )
139 138 rspcev ⊢ ( ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) ∈ Ons ∧ ( ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝐴 ∧ ¬ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) |s ∅ ) <s 𝑦 ) ) → ∃ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 ∧ ¬ 𝑧 <s 𝑦 ) )
140 41 88 134 139 syl12anc ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) ∧ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) → ∃ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 ∧ ¬ 𝑧 <s 𝑦 ) )
141 140 ex ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) → ∃ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 ∧ ¬ 𝑧 <s 𝑦 ) ) )
142 ontri1 ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝑦 ) ∈ On ) → ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ↔ ¬ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) )
143 71 51 142 mp2an ⊢ ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ↔ ¬ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) )
144 143 con2bii ⊢ ( ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ↔ ¬ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) )
145 rexanali ⊢ ( ∃ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 ∧ ¬ 𝑧 <s 𝑦 ) ↔ ¬ ∀ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 → 𝑧 <s 𝑦 ) )
146 141 144 145 3imtr3g ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) → ( ¬ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) → ¬ ∀ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 → 𝑧 <s 𝑦 ) ) )
147 146 con4d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) → ( ∀ 𝑧 ∈ Ons ( 𝑧 <s 𝐴 → 𝑧 <s 𝑦 ) → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ) )
148 31 147 syl5 ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) → ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ) )
149 148 adantrd ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑦 ∈ No ) → ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ) )
150 149 ralrimiva ⊢ ( 𝐴 ∈ Ons → ∀ 𝑦 ∈ No ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ) )
151 3 8 elpwd ⊢ ( 𝐴 ∈ Ons → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∈ 𝒫 No )
152 nulssgt ⊢ ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∈ 𝒫 No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s ∅ )
153 151 152 syl ⊢ ( 𝐴 ∈ Ons → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s ∅ )
154 eqscut2 ⊢ ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s ∅ ∧ 𝐴 ∈ No ) → ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) = 𝐴 ↔ ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝐴 } ∧ { 𝐴 } <<s ∅ ∧ ∀ 𝑦 ∈ No ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ) ) ) )
155 153 1 154 syl2anc ⊢ ( 𝐴 ∈ Ons → ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) = 𝐴 ↔ ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝐴 } ∧ { 𝐴 } <<s ∅ ∧ ∀ 𝑦 ∈ No ( ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑦 ) ) ) ) )
156 19 22 150 155 mpbir3and ⊢ ( 𝐴 ∈ Ons → ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) = 𝐴 )
157 156 eqcomd ⊢ ( 𝐴 ∈ Ons → 𝐴 = ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) )