Metamath Proof Explorer

Theorem madebdaylemlrcut

Description: Lemma for madebday . If the inductive hypothesis of madebday is satisfied up to the birthday of X , then the conclusion of lrcut holds. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebdaylemlrcut ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ssltleft ⊢ ( 𝑋 ∈ No → ( L ‘ 𝑋 ) <<s { 𝑋 } )
2 1 adantl ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( L ‘ 𝑋 ) <<s { 𝑋 } )
3 ssltright ⊢ ( 𝑋 ∈ No → { 𝑋 } <<s ( R ‘ 𝑋 ) )
4 3 adantl ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → { 𝑋 } <<s ( R ‘ 𝑋 ) )
5 fveq2 ⊢ ( 𝑋 = 𝑤 → ( bday ‘ 𝑋 ) = ( bday ‘ 𝑤 ) )
6 eqimss ⊢ ( ( bday ‘ 𝑋 ) = ( bday ‘ 𝑤 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) )
7 5 6 syl ⊢ ( 𝑋 = 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) )
8 7 a1i ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) ) ) → ( 𝑋 = 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
9 ssltsep ⊢ ( ( L ‘ 𝑋 ) <<s { 𝑤 } → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∀ 𝑦 ∈ { 𝑤 } 𝑥 <s 𝑦 )
10 vex ⊢ 𝑤 ∈ V
11 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑤 ) )
12 10 11 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑤 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑤 )
13 12 ralbii ⊢ ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∀ 𝑦 ∈ { 𝑤 } 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 )
14 9 13 sylib ⊢ ( ( L ‘ 𝑋 ) <<s { 𝑤 } → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 )
15 ssltsep ⊢ ( { 𝑤 } <<s ( R ‘ 𝑋 ) → ∀ 𝑦 ∈ { 𝑤 } ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑦 <s 𝑥 )
16 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 <s 𝑥 ↔ 𝑤 <s 𝑥 ) )
17 16 ralbidv ⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑦 <s 𝑥 ↔ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) )
18 10 17 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑤 } ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑦 <s 𝑥 ↔ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 )
19 15 18 sylib ⊢ ( { 𝑤 } <<s ( R ‘ 𝑋 ) → ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 )
20 14 19 anim12i ⊢ ( ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) )
21 leftval ⊢ ( L ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑧 <s 𝑋 }
22 21 a1i ⊢ ( 𝑋 ∈ No → ( L ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑧 <s 𝑋 } )
23 22 raleqdv ⊢ ( 𝑋 ∈ No → ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ↔ ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑧 <s 𝑋 } 𝑥 <s 𝑤 ) )
24 rightval ⊢ ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 }
25 24 a1i ⊢ ( 𝑋 ∈ No → ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } )
26 25 raleqdv ⊢ ( 𝑋 ∈ No → ( ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ↔ ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } 𝑤 <s 𝑥 ) )
27 23 26 anbi12d ⊢ ( 𝑋 ∈ No → ( ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) ↔ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑧 <s 𝑋 } 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } 𝑤 <s 𝑥 ) ) )
28 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 <s 𝑋 ↔ 𝑥 <s 𝑋 ) )
29 28 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑧 <s 𝑋 } 𝑥 <s 𝑤 ↔ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) )
30 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑋 <s 𝑧 ↔ 𝑋 <s 𝑥 ) )
31 30 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } 𝑤 <s 𝑥 ↔ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) )
32 29 31 anbi12i ⊢ ( ( ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑧 <s 𝑋 } 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } 𝑤 <s 𝑥 ) ↔ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) )
33 27 32 bitrdi ⊢ ( 𝑋 ∈ No → ( ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) ↔ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) )
34 33 ad2antlr ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ 𝑤 ∈ No ) → ( ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) ↔ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) )
35 simplrl ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → 𝑤 ∈ No )
36 sltirr ⊢ ( 𝑤 ∈ No → ¬ 𝑤 <s 𝑤 )
37 35 36 syl ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ¬ 𝑤 <s 𝑤 )
38 bdayelon ⊢ ( bday ‘ 𝑋 ) ∈ On
39 bdayelon ⊢ ( bday ‘ 𝑤 ) ∈ On
40 ontri1 ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑤 ) ∈ On ) → ( ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ) )
41 38 39 40 mp2an ⊢ ( ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) )
42 41 con2bii ⊢ ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) ↔ ¬ ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) )
43 simplll ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
44 madebdaylemold ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑤 ∈ No ) → ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) → 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ) )
45 38 43 35 44 mp3an2i ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) → 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ) )
46 slttrine ⊢ ( ( 𝑋 ∈ No ∧ 𝑤 ∈ No ) → ( 𝑋 ≠ 𝑤 ↔ ( 𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋 ) ) )
47 46 ad2ant2lr ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑋 ≠ 𝑤 ↔ ( 𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋 ) ) )
48 simprrr ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) )
49 breq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑋 <s 𝑥 ↔ 𝑋 <s 𝑤 ) )
50 breq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑤 <s 𝑥 ↔ 𝑤 <s 𝑤 ) )
51 49 50 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ↔ ( 𝑋 <s 𝑤 → 𝑤 <s 𝑤 ) ) )
52 51 rspccv ⊢ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → ( 𝑋 <s 𝑤 → 𝑤 <s 𝑤 ) ) )
53 48 52 syl ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → ( 𝑋 <s 𝑤 → 𝑤 <s 𝑤 ) ) )
54 53 com23 ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑋 <s 𝑤 → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑤 <s 𝑤 ) ) )
55 simprrl ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) )
56 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 <s 𝑋 ↔ 𝑤 <s 𝑋 ) )
57 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 <s 𝑤 ↔ 𝑤 <s 𝑤 ) )
58 56 57 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ↔ ( 𝑤 <s 𝑋 → 𝑤 <s 𝑤 ) ) )
59 58 rspccv ⊢ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → ( 𝑤 <s 𝑋 → 𝑤 <s 𝑤 ) ) )
60 55 59 syl ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → ( 𝑤 <s 𝑋 → 𝑤 <s 𝑤 ) ) )
61 60 com23 ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑤 <s 𝑋 → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑤 <s 𝑤 ) ) )
62 54 61 jaod ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( ( 𝑋 <s 𝑤 ∨ 𝑤 <s 𝑋 ) → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑤 <s 𝑤 ) ) )
63 47 62 sylbid ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑋 ≠ 𝑤 → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑤 <s 𝑤 ) ) )
64 63 imp ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ( 𝑤 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑤 <s 𝑤 ) )
65 45 64 syld ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ( ( bday ‘ 𝑤 ) ∈ ( bday ‘ 𝑋 ) → 𝑤 <s 𝑤 ) )
66 42 65 biimtrrid ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ( ¬ ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) → 𝑤 <s 𝑤 ) )
67 37 66 mt3d ⊢ ( ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) ∧ 𝑋 ≠ 𝑤 ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) )
68 67 ex ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) ) ) → ( 𝑋 ≠ 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
69 68 expr ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ 𝑤 ∈ No ) → ( ( ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑥 <s 𝑋 → 𝑥 <s 𝑤 ) ∧ ∀ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ( 𝑋 <s 𝑥 → 𝑤 <s 𝑥 ) ) → ( 𝑋 ≠ 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) ) )
70 34 69 sylbid ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ 𝑤 ∈ No ) → ( ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) → ( 𝑋 ≠ 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) ) )
71 70 impr ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) 𝑥 <s 𝑤 ∧ ∀ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑤 <s 𝑥 ) ) ) → ( 𝑋 ≠ 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
72 20 71 sylanr2 ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) ) ) → ( 𝑋 ≠ 𝑤 → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
73 8 72 pm2.61dne ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ ( 𝑤 ∈ No ∧ ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) ) ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) )
74 73 expr ⊢ ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) ∧ 𝑤 ∈ No ) → ( ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
75 74 ralrimiva ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ∀ 𝑤 ∈ No ( ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
76 bdayfn ⊢ bday Fn No
77 ssrab2 ⊢ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ⊆ No
78 fnssintima ⊢ ( ( bday Fn No ∧ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ⊆ No ) → ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ↔ ∀ 𝑤 ∈ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
79 76 77 78 mp2an ⊢ ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ↔ ∀ 𝑤 ∈ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) )
80 sneq ⊢ ( 𝑧 = 𝑤 → { 𝑧 } = { 𝑤 } )
81 80 breq2d ⊢ ( 𝑧 = 𝑤 → ( ( L ‘ 𝑋 ) <<s { 𝑧 } ↔ ( L ‘ 𝑋 ) <<s { 𝑤 } ) )
82 80 breq1d ⊢ ( 𝑧 = 𝑤 → ( { 𝑧 } <<s ( R ‘ 𝑋 ) ↔ { 𝑤 } <<s ( R ‘ 𝑋 ) ) )
83 81 82 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) ↔ ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) ) )
84 83 ralrab ⊢ ( ∀ 𝑤 ∈ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ↔ ∀ 𝑤 ∈ No ( ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
85 79 84 bitri ⊢ ( ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ↔ ∀ 𝑤 ∈ No ( ( ( L ‘ 𝑋 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ( R ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑤 ) ) )
86 75 85 sylibr ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( bday ‘ 𝑋 ) ⊆ ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) )
87 sneq ⊢ ( 𝑧 = 𝑋 → { 𝑧 } = { 𝑋 } )
88 87 breq2d ⊢ ( 𝑧 = 𝑋 → ( ( L ‘ 𝑋 ) <<s { 𝑧 } ↔ ( L ‘ 𝑋 ) <<s { 𝑋 } ) )
89 87 breq1d ⊢ ( 𝑧 = 𝑋 → ( { 𝑧 } <<s ( R ‘ 𝑋 ) ↔ { 𝑋 } <<s ( R ‘ 𝑋 ) ) )
90 88 89 anbi12d ⊢ ( 𝑧 = 𝑋 → ( ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) ↔ ( ( L ‘ 𝑋 ) <<s { 𝑋 } ∧ { 𝑋 } <<s ( R ‘ 𝑋 ) ) ) )
91 simpr ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → 𝑋 ∈ No )
92 2 4 jca ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( L ‘ 𝑋 ) <<s { 𝑋 } ∧ { 𝑋 } <<s ( R ‘ 𝑋 ) ) )
93 90 91 92 elrabd ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → 𝑋 ∈ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } )
94 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ⊆ No ∧ 𝑋 ∈ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) → ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) )
95 76 77 93 94 mp3an12i ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) )
96 intss1 ⊢ ( ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) → ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ⊆ ( bday ‘ 𝑋 ) )
97 95 96 syl ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ⊆ ( bday ‘ 𝑋 ) )
98 86 97 eqssd ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) )
99 lltropt ⊢ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
100 eqscut ⊢ ( ( ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) ∧ 𝑋 ∈ No ) → ( ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 ↔ ( ( L ‘ 𝑋 ) <<s { 𝑋 } ∧ { 𝑋 } <<s ( R ‘ 𝑋 ) ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ) ) )
101 99 100 mpan ⊢ ( 𝑋 ∈ No → ( ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 ↔ ( ( L ‘ 𝑋 ) <<s { 𝑋 } ∧ { 𝑋 } <<s ( R ‘ 𝑋 ) ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ) ) )
102 101 adantl ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 ↔ ( ( L ‘ 𝑋 ) <<s { 𝑋 } ∧ { 𝑋 } <<s ( R ‘ 𝑋 ) ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑧 ∈ No ∣ ( ( L ‘ 𝑋 ) <<s { 𝑧 } ∧ { 𝑧 } <<s ( R ‘ 𝑋 ) ) } ) ) ) )
103 2 4 98 102 mpbir3and ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )