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 biimtrrid ⊢ ∀ 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 ⊢ 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 mpan ⊢ 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