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 
 |-  ( _L ` X ) = { z e. ( _Old ` ( bday ` X ) ) | z
22 21 a1i 
 |-  ( X e. No -> ( _L ` X ) = { z e. ( _Old ` ( bday ` X ) ) | z
23 22 raleqdv 
 |-  ( X e. No -> ( A. x e. ( _L ` X ) x  A. x e. { z e. ( _Old ` ( bday ` X ) ) | z
24 rightval 
 |-  ( _R ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
25 24 a1i 
 |-  ( X e. No -> ( _R ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
26 25 raleqdv 
 |-  ( X e. No -> ( A. x e. ( _R ` X ) w  A. x e. { z e. ( _Old ` ( bday ` X ) ) | X
27 23 26 anbi12d 
 |-  ( X e. No -> ( ( A. x e. ( _L ` X ) x  ( A. x e. { z e. ( _Old ` ( bday ` X ) ) | z
28 breq1 
 |-  ( z = x -> ( z  x
29 28 ralrab 
 |-  ( A. x e. { z e. ( _Old ` ( bday ` X ) ) | z  A. x e. ( _Old ` ( bday ` X ) ) ( x  x
30 breq2 
 |-  ( z = x -> ( X  X
31 30 ralrab 
 |-  ( A. x e. { z e. ( _Old ` ( bday ` X ) ) | X  A. x e. ( _Old ` ( bday ` X ) ) ( X  w
32 29 31 anbi12i 
 |-  ( ( A. x e. { z e. ( _Old ` ( bday ` X ) ) | z  ( A. x e. ( _Old ` ( bday ` X ) ) ( x  x  w
33 27 32 bitrdi 
 |-  ( X e. No -> ( ( A. x e. ( _L ` X ) x  ( A. x e. ( _Old ` ( bday ` X ) ) ( x  x  w
34 33 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
35 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 )
36 sltirr 
 |-  ( w e. No -> -. w
37 35 36 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
38 bdayelon 
 |-  ( bday ` X ) e. On
39 bdayelon 
 |-  ( bday ` w ) e. On
40 ontri1 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` w ) e. On ) -> ( ( bday ` X ) C_ ( bday ` w ) <-> -. ( bday ` w ) e. ( bday ` X ) ) )
41 38 39 40 mp2an 
 |-  ( ( bday ` X ) C_ ( bday ` w ) <-> -. ( bday ` w ) e. ( bday ` X ) )
42 41 con2bii 
 |-  ( ( bday ` w ) e. ( bday ` X ) <-> -. ( bday ` X ) C_ ( bday ` w ) )
43 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 ) ) )
44 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 ) ) ) )
45 38 43 35 44 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 ) ) ) )
46 slttrine 
 |-  ( ( X e. No /\ w e. No ) -> ( X =/= w <-> ( X
47 46 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
48 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
49 breq2 
 |-  ( x = w -> ( X  X
50 breq2 
 |-  ( x = w -> ( w  w
51 49 50 imbi12d 
 |-  ( x = w -> ( ( X  w  ( X  w
52 51 rspccv 
 |-  ( A. x e. ( _Old ` ( bday ` X ) ) ( X  w  ( w e. ( _Old ` ( bday ` X ) ) -> ( X  w
53 48 52 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
54 53 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
55 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
56 breq1 
 |-  ( x = w -> ( x  w
57 breq1 
 |-  ( x = w -> ( x  w
58 56 57 imbi12d 
 |-  ( x = w -> ( ( x  x  ( w  w
59 58 rspccv 
 |-  ( A. x e. ( _Old ` ( bday ` X ) ) ( x  x  ( w e. ( _Old ` ( bday ` X ) ) -> ( w  w
60 55 59 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
61 60 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
62 54 61 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
63 47 62 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
64 63 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
65 45 64 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
66 42 65 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
67 37 66 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 ) )
68 67 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 ) ) )
69 68 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 ) ) ) )
70 34 69 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 ) ) ) )
71 70 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 ) ) )
72 20 71 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 ) ) )
73 8 72 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 ) )
74 73 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 ) ) )
75 74 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 ) ) )
76 bdayfn 
 |-  bday Fn No
77 ssrab2 
 |-  { z e. No | ( ( _L ` X ) <
78 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 ) <
79 76 77 78 mp2an 
 |-  ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _L ` X ) < A. w e. { z e. No | ( ( _L ` X ) <
80 sneq 
 |-  ( z = w -> { z } = { w } )
81 80 breq2d 
 |-  ( z = w -> ( ( _L ` X ) < ( _L ` X ) <
82 80 breq1d 
 |-  ( z = w -> ( { z } < { w } <
83 81 82 anbi12d 
 |-  ( z = w -> ( ( ( _L ` X ) < ( ( _L ` X ) <
84 83 ralrab 
 |-  ( A. w e. { z e. No | ( ( _L ` X ) < A. w e. No ( ( ( _L ` X ) < ( bday ` X ) C_ ( bday ` w ) ) )
85 79 84 bitri 
 |-  ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _L ` X ) < A. w e. No ( ( ( _L ` X ) < ( bday ` X ) C_ ( bday ` w ) ) )
86 75 85 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 ) <
87 sneq 
 |-  ( z = X -> { z } = { X } )
88 87 breq2d 
 |-  ( z = X -> ( ( _L ` X ) < ( _L ` X ) <
89 87 breq1d 
 |-  ( z = X -> ( { z } < { X } <
90 88 89 anbi12d 
 |-  ( z = X -> ( ( ( _L ` X ) < ( ( _L ` X ) <
91 simpr 
 |-  ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> X e. No )
92 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 ) <
93 90 91 92 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 ) <
94 fnfvima 
 |-  ( ( bday Fn No /\ { z e. No | ( ( _L ` X ) < ( bday ` X ) e. ( bday " { z e. No | ( ( _L ` X ) <
95 76 77 93 94 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 ) <
96 intss1 
 |-  ( ( bday ` X ) e. ( bday " { z e. No | ( ( _L ` X ) < |^| ( bday " { z e. No | ( ( _L ` X ) <
97 95 96 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 ) <
98 86 97 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 ) <
99 lltropt 
 |-  ( X e. No -> ( _L ` X ) <
100 eqscut 
 |-  ( ( ( _L ` X ) < ( ( ( _L ` X ) |s ( _R ` X ) ) = X <-> ( ( _L ` X ) <
101 99 100 mpancom 
 |-  ( X e. No -> ( ( ( _L ` X ) |s ( _R ` X ) ) = X <-> ( ( _L ` X ) <
102 101 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 ) <
103 2 4 98 102 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 )