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 
|- ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( ( _L ` X ) |s ( _R ` X ) ) = X )

Proof

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