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 syl5bir ( ( ( ( ∀ 𝑏 ∈ ( 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 ( 𝑋 No → ( 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 mpancom ( 𝑋 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 ‘ 𝑋 ) ) = 𝑋 )