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 b bday X y No bday y b y M b X No L X | s R X = X

Proof

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